Documentation

Mathlib.Tactic.Nontriviality.Core

The nontriviality tactic. #

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

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
    Instances For

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

      Equations
        Instances For

          Attempts to generate a Nontrivial α hypothesis.

          The tactic first checks to see that there is not already a Nontrivial α instance before trying to synthesize one using other techniques.

          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 α, and attempt to discharge the Subsingleton goal using simp [h₁, h₂, ..., hₙ, nontriviality], where [h₁, h₂, ..., hₙ] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using h₁, h₂, ..., hₙ.

          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
            Instances For