mathlib documentation

tactic.dec_trivial

dec_trivial tactic #

The dec_trivial tactic tries to use decidability to prove a goal. It is basically a glorified wrapper around exact dec_trivial.

There is an extra option to make it a little bit smarter: dec_trivial! will revert all hypotheses on which the target depends, before it tries exact dec_trivial.

source
meta def tactic.interactive.dec_trivial (revert_deps : interactive.parse (lean.parser.tk "!")?) :
tactic unit

dec_trivial tries to use decidability to prove a goal (i.e., using exact dec_trivial). The variant dec_trivial! will revert all hypotheses on which the target depends, before it tries exact dec_trivial.

Example:

example (n : ℕ) (h : n < 2) : n = 0 ∨ n = 1 :=
by dec_trivial!