theorem Lean.Grind.intro_with_eq (p p' q : Prop) (he : p = p') (h : p' → q) : p → q

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.and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∧ b) = False

theorem Lean.Grind.and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = False

theorem Lean.Grind.eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True

theorem Lean.Grind.eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True

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_true_right {a b : Prop} (h : b = 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

theorem Lean.Grind.eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False

theorem Lean.Grind.eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False

Not

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

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

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

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

theorem Lean.Grind.false_of_not_eq_self {a : Prop} (h : (¬a) = a) : False

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₂)

Forall

theorem Lean.Grind.forall_propagator (p : Prop) (q : p → Prop) (q' : Prop) (h₁ : p = True) (h₂ : q ⋯ = q') : (∀ (hp : p), q hp) = q'

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