The nontriviality tactic.

theorem Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim {p : Prop} {α : Type u} (h₁ : Subsingleton α → p) (h₂ : Nontrivial α → p) : p

def Mathlib.Tactic.Nontriviality.nontrivialityByElim {u : Lean.Level} (α : Q(Type u)) (g : Lean.MVarId) (simpArgs : Array Lean.Syntax) : Lean.MetaM Lean.MVarId

Tries to generate a Nontrivial α instance by performing case analysis on subsingleton_or_nontrivial α, attempting to discharge the subsingleton branch using lemmas with @[nontriviality] attribute, including Subsingleton.le and eq_iff_true_of_subsingleton.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Nontriviality.nontrivialityByAssumption (g : Lean.MVarId) : Lean.MetaM Unit

Tries to generate a Nontrivial α instance using nontrivial_of_ne or nontrivial_of_lt and local hypotheses.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Nontriviality.nontriviality : Lean.ParserDescr

nontriviality α generates a proof of Nontrivial α and adds this as a hypothesis.

The tactic first tries to find a proof of Nontrivial α using instance synthesis. If this fails, it will derive this proof using a < b, a ≠ b or a > b hypotheses in the local context. Otherwise it will perform a case split on Subsingleton α ∨ Nontrivial α, and attempt to prove Subsingleton α implies the main goal using simp [nontriviality]. If the Subsingleton goal cannot be closed automatically, nontriviality fails.

This tactic is extensible: tag a lemma with @[nontriviality] to use it in the simp set for the Subsingleton case. All @[simp] lemmas are automatically used too.

• nontriviality (without the argument α) infers the type from the main goal, if the goal is an (in)equality.
• nontriviality using h₁, h₂, ..., hₙ uses h₁, ..., hₙ as extra arguments to simp in the Subsingleton case. This supports the typical simp argument syntax: nontriviality using ← h rewrites right-to-left with this argument; nontriviality using -h removes a lemma from the default simp set for this tactic invocation. nontriviality using * adds all local hypotheses to the simp set.

Examples:

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 0 < a := by
  nontriviality -- There is now a `Nontrivial R` hypothesis available.
  assumption

example {R : Type} [CommRing R] {r s : R} : r * s = s * r := by
  nontriviality -- There is now a `Nontrivial R` hypothesis available.
  apply mul_comm

example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : (2 : ℕ) ∣ 4 := by
  nontriviality R -- there is now a `Nontrivial R` hypothesis available.
  dec_trivial

def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b := by
  success_if_fail nontriviality α -- Fails
  nontriviality α using myeq -- There is now a `Nontrivial α` hypothesis available
  assumption

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Nontriviality.elabNontriviality : Lean.Elab.Tactic.Tactic

Elaborator for the nontriviality tactic.

Equations

• One or more equations did not get rendered due to their size.