Documentation

Init.Grind.Lemmas

def Lean.Grind.intro_with_eq (p p' : Prop) (q : Sort u) (he : p = p') (h : p'q) :
pq
Equations
    Instances For
      def Lean.Grind.intro_with_eq' (p p' : Prop) (q : pSort u) (he : p = p') (h : (h : p') → q ) (h✝ : p) :
      q h✝
      Equations
        Instances For

          And

          theorem Lean.Grind.and_eq_of_eq_true_left {a b : Prop} (h : a = True) :
          (a b) = b
          theorem Lean.Grind.and_eq_of_eq_true_right {a b : Prop} (h : b = True) :
          (a b) = a
          theorem Lean.Grind.or_of_and_eq_false {a b : Prop} (h : (a b) = False) :

          Or

          theorem Lean.Grind.or_eq_of_eq_true_left {a b : Prop} (h : a = True) :
          (a b) = True
          theorem Lean.Grind.or_eq_of_eq_false_left {a b : Prop} (h : a = False) :
          (a b) = b
          theorem Lean.Grind.or_eq_of_eq_false_right {a b : Prop} (h : b = False) :
          (a b) = a

          Implies

          theorem Lean.Grind.imp_eq_of_eq_false_left {a b : Prop} (h : a = False) :
          (ab) = True
          theorem Lean.Grind.imp_eq_of_eq_true_right {a b : Prop} (h : b = True) :
          (ab) = True
          theorem Lean.Grind.imp_eq_of_eq_true_left {a b : Prop} (h : a = True) :
          (ab) = b
          theorem Lean.Grind.eq_false_of_imp_eq_true {a b : Prop} (h₁ : (ab) = True) (h₂ : b = False) :
          theorem Lean.Grind.eq_true_of_imp_eq_false {a b : Prop} (h : (ab) = False) :
          theorem Lean.Grind.eq_false_of_imp_eq_false {a b : Prop} (h : (ab) = False) :

          Not

          Eq

          theorem Lean.Grind.eq_eq_of_eq_true_left {a b : Prop} (h : a = True) :
          (a = b) = b
          theorem Lean.Grind.eq_eq_of_eq_true_right {a b : Prop} (h : b = True) :
          (a = b) = a
          theorem Lean.Grind.eq_congr {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = a₂) (h₂ : b₁ = b₂) :
          (a₁ = b₁) = (a₂ = b₂)
          theorem Lean.Grind.eq_congr' {α : Sort u} {a₁ b₁ a₂ b₂ : α} (h₁ : a₁ = b₂) (h₂ : b₁ = a₂) :
          (a₁ = b₁) = (a₂ = b₂)

          Ne

          theorem Lean.Grind.ne_of_ne_of_eq_left {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b c) :
          a c
          theorem Lean.Grind.ne_of_ne_of_eq_right {α : Sort u} {a b c : α} (h₁ : a = c) (h₂ : b c) :
          b a

          BEq

          theorem Lean.Grind.beq_eq_true_of_eq {α : Type u} {x✝ : BEq α} :
          ∀ {x : LawfulBEq α} {a b : α} (h : a = b), (a == b) = true
          theorem Lean.Grind.beq_eq_false_of_diseq {α : Type u} {x✝ : BEq α} :
          ∀ {x : LawfulBEq α} {a b : α} (h : ¬a = b), (a == b) = false
          theorem Lean.Grind.eq_of_beq_eq_true {α : Type u} {x✝ : BEq α} :
          ∀ {x : LawfulBEq α} {a b : α} (h : (a == b) = true), a = b
          theorem Lean.Grind.ne_of_beq_eq_false {α : Type u} {x✝ : BEq α} :
          ∀ {x : LawfulBEq α} {a b : α} (h : (a == b) = false), (a = b) = False

          Bool.and

          theorem Lean.Grind.Bool.and_eq_of_eq_true_left {a b : Bool} (h : a = true) :
          (a && b) = b
          theorem Lean.Grind.Bool.and_eq_of_eq_true_right {a b : Bool} (h : b = true) :
          (a && b) = a

          Bool.or

          theorem Lean.Grind.Bool.or_eq_of_eq_false_left {a b : Bool} (h : a = false) :
          (a || b) = b

          Bool.not

          theorem Lean.Grind.of_eq_eq_true {a b : Prop} (h : (a = b) = True) :
          a b ¬a ¬b
          theorem Lean.Grind.of_eq_eq_false {a b : Prop} (h : (a = b) = False) :
          a ¬b ¬a b

          Forall

          theorem Lean.Grind.forall_propagator (p : Prop) (q : pProp) (q' : Prop) (h₁ : p = True) (h₂ : q = q') :
          (∀ (hp : p), q hp) = q'
          theorem Lean.Grind.of_forall_eq_false (α : Sort u) (p : αProp) (h : (∀ (x : α), p x) = False) :
          (x : α), ¬p x

          dite

          theorem Lean.Grind.dite_cond_eq_true' {α : Sort u} {c : Prop} {x✝ : Decidable c} {a : cα} {b : ¬cα} {r : α} (h₁ : c = True) (h₂ : a = r) :
          dite c a b = r
          theorem Lean.Grind.dite_cond_eq_false' {α : Sort u} {c : Prop} {x✝ : Decidable c} {a : cα} {b : ¬cα} {r : α} (h₁ : c = False) (h₂ : b = r) :
          dite c a b = r

          Casts

          theorem Lean.Grind.eqRec_heq {α : Sort u_2} {a : α} {motive : (x : α) → a = xSort u_1} (v : motive a ) {b : α} (h : a = b) :
          h v v
          theorem Lean.Grind.eqRecOn_heq {α : Sort u_2} {a : α} {motive : (x : α) → a = xSort u_1} {b : α} (h : a = b) (v : motive a ) :
          theorem Lean.Grind.eqNDRec_heq {α : Sort u_2} {a : α} {motive : αSort u_1} (v : motive a) {b : α} (h : a = b) :
          h v v

          decide

          theorem Lean.Grind.decide_eq_true {p : Prop} {x✝ : Decidable p} :
          p = Truedecide p = true

          Lookahead

          theorem Lean.Grind.of_lookahead (p : Prop) (h : ¬pFalse) :