Lemmas use by the congruence closure module

theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ↔ b) = b

theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ↔ b) = a

theorem Mathlib.Tactic.CC.iff_eq_true_of_eq {a b : Prop} (h : a = b) : (a ↔ b) = True

theorem Mathlib.Tactic.CC.and_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∧ b) = b

theorem Mathlib.Tactic.CC.and_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∧ b) = a

theorem Mathlib.Tactic.CC.and_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∧ b) = False

theorem Mathlib.Tactic.CC.and_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∧ b) = False

theorem Mathlib.Tactic.CC.and_eq_of_eq {a b : Prop} (h : a = b) : (a ∧ b) = a

theorem Mathlib.Tactic.CC.or_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a ∨ b) = True

theorem Mathlib.Tactic.CC.or_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a ∨ b) = True

theorem Mathlib.Tactic.CC.or_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a ∨ b) = b

theorem Mathlib.Tactic.CC.or_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a ∨ b) = a

theorem Mathlib.Tactic.CC.or_eq_of_eq {a b : Prop} (h : a = b) : (a ∨ b) = a

theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_left {a b : Prop} (h : a = True) : (a → b) = b

theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_right {a b : Prop} (h : b = True) : (a → b) = True

theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_left {a b : Prop} (h : a = False) : (a → b) = True

theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_right {a b : Prop} (h : b = False) : (a → b) = ¬a

theorem Mathlib.Tactic.CC.not_imp_eq_of_eq_false_right {a b : Prop} (h : b = False) : (¬a → b) = a

theorem Mathlib.Tactic.CC.imp_eq_true_of_eq {a b : Prop} (h : a = b) : (a → b) = True

theorem Mathlib.Tactic.CC.not_eq_of_eq_true {a : Prop} (h : a = True) : (¬a) = False

theorem Mathlib.Tactic.CC.not_eq_of_eq_false {a : Prop} (h : a = False) : (¬a) = True

theorem Mathlib.Tactic.CC.false_of_a_eq_not_a {a : Prop} (h : a = ¬a) : False

theorem Mathlib.Tactic.CC.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 Mathlib.Tactic.CC.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 Mathlib.Tactic.CC.if_eq_of_eq (c : Prop) [d : Decidable c] {α : Sort u} {t e : α} (h : t = e) : (if c then t else e) = t

theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) : a = True

theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) : b = True

theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) : a = False

theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) : b = False

theorem Mathlib.Tactic.CC.eq_false_of_not_eq_true {a : Prop} (h : (¬a) = True) : a = False

theorem Mathlib.Tactic.CC.eq_true_of_not_eq_false {a : Prop} (h : (¬a) = False) : a = True