Lemmas use by the congruence closure module

theorem iff_eq_of_eq_true_left {a : Prop} {b : Prop} (h : a = True) : (a ↔ b) = b

theorem iff_eq_of_eq_true_right {a : Prop} {b : Prop} (h : b = True) : (a ↔ b) = a

theorem iff_eq_true_of_eq {a : Prop} {b : Prop} (h : a = b) : (a ↔ b) = True

theorem and_eq_of_eq_true_left {a : Prop} {b : Prop} (h : a = True) : (a ∧ b) = b

theorem and_eq_of_eq_true_right {a : Prop} {b : Prop} (h : b = True) : (a ∧ b) = a

theorem and_eq_of_eq_false_left {a : Prop} {b : Prop} (h : a = False) : (a ∧ b) = False

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

theorem and_eq_of_eq {a : Prop} {b : Prop} (h : a = b) : (a ∧ b) = a

theorem or_eq_of_eq_true_left {a : Prop} {b : Prop} (h : a = True) : (a ∨ b) = True

theorem or_eq_of_eq_true_right {a : Prop} {b : Prop} (h : b = True) : (a ∨ b) = True

theorem or_eq_of_eq_false_left {a : Prop} {b : Prop} (h : a = False) : (a ∨ b) = b

theorem or_eq_of_eq_false_right {a : Prop} {b : Prop} (h : b = False) : (a ∨ b) = a

theorem or_eq_of_eq {a : Prop} {b : Prop} (h : a = b) : (a ∨ b) = a

theorem imp_eq_of_eq_true_left {a : Prop} {b : Prop} (h : a = True) : (a → b) = b

theorem imp_eq_of_eq_true_right {a : Prop} {b : Prop} (h : b = True) : (a → b) = True

theorem imp_eq_of_eq_false_left {a : Prop} {b : Prop} (h : a = False) : (a → b) = True

theorem imp_eq_of_eq_false_right {a : Prop} {b : Prop} (h : b = False) : (a → b) = ¬a

theorem not_imp_eq_of_eq_false_right {a : Prop} {b : Prop} (h : b = False) : (¬a → b) = a

theorem imp_eq_true_of_eq {a : Prop} {b : Prop} (h : a = b) : (a → b) = True

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

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

theorem false_of_a_eq_not_a {a : Prop} (h : a = ¬a) : False

theorem if_eq_of_eq_true {c : Prop} [d : Decidable c] {α : Sort u} (t : α) (e : α) (h : c = True) : (if c then t else e) = t

theorem if_eq_of_eq_false {c : Prop} [d : Decidable c] {α : Sort u} (t : α) (e : α) (h : c = False) : (if c then t else e) = e

theorem if_eq_of_eq (c : Prop) [d : Decidable c] {α : Sort u} {t : α} {e : α} (h : t = e) : (if c then t else e) = t

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

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

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

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

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

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

theorem ne_of_eq_of_ne {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c

theorem Eq.trans_ne {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a = b) (h₂ : b ≠ c) : a ≠ c

Alias of ne_of_eq_of_ne.

theorem ne_of_ne_of_eq {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c

theorem Ne.trans_eq {α : Sort u} {a : α} {b : α} {c : α} (h₁ : a ≠ b) (h₂ : b = c) : a ≠ c

Alias of ne_of_ne_of_eq.