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_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

      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) :
      HEq (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 ) :
      HEq (Eq.recOn h v) v
      theorem Lean.Grind.eqNDRec_heq {α : Sort u_2} {a : α} {motive : αSort u_1} (v : motive a) {b : α} (h : a = b) :
      HEq (h v) v

      decide

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