The nontriviality tactic.

ink

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

The @[nontriviality] simp set is used by the nontriviality tactic to automatically discharge theorems about the trivial case (where we know Subsingleton α and many theorems in e.g. groups are trivially true).

Equations

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

ink

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

ink

def Mathlib.Tactic.Nontriviality.nontrivialityByElim {u : Lean.Level} (α : Qq.QQ (Lean.Expr.sort (Lean.Level.succ 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.

ink

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.

ink

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

Attempts to generate a Nontrivial α hypothesis.

The tactic first looks for an instance using infer_instance.

If the goal is an (in)equality, the type α is inferred from the goal. Otherwise, the type needs to be specified in the tactic invocation, as nontriviality α.

The nontriviality tactic will first look for strict inequalities amongst the hypotheses, and use these to derive the Nontrivial instance directly.

Otherwise, it will perform a case split on Subsingleton α ∨ Nontrivial α∨ Nontrivial α, and attempt to discharge the Subsingleton goal using simp [lemmas, nontriviality], where [lemmas] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using [lemmas].

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
∣ 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.

ink

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.