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.

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!

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!