Lemmas use by the congruence closure module

source
theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_left {a b : Prop} (h : a = True) :
(a ↔ b) = b
source
theorem Mathlib.Tactic.CC.iff_eq_of_eq_true_right {a b : Prop} (h : b = True) :
(a ↔ b) = a
source
theorem Mathlib.Tactic.CC.iff_eq_true_of_eq {a b : Prop} (h : a = b) :
(a ↔ b) = True
source
theorem Mathlib.Tactic.CC.and_eq_of_eq_true_left {a b : Prop} (h : a = True) :
(a ∧ b) = b
source
theorem Mathlib.Tactic.CC.and_eq_of_eq_true_right {a b : Prop} (h : b = True) :
(a ∧ b) = a
source
theorem Mathlib.Tactic.CC.and_eq_of_eq_false_left {a b : Prop} (h : a = False) :
(a ∧ b) = False
source
theorem Mathlib.Tactic.CC.and_eq_of_eq_false_right {a b : Prop} (h : b = False) :
(a ∧ b) = False
source
theorem Mathlib.Tactic.CC.and_eq_of_eq {a b : Prop} (h : a = b) :
(a ∧ b) = a
source
theorem Mathlib.Tactic.CC.or_eq_of_eq_true_left {a b : Prop} (h : a = True) :
(a ∨ b) = True
source
theorem Mathlib.Tactic.CC.or_eq_of_eq_true_right {a b : Prop} (h : b = True) :
(a ∨ b) = True
source
theorem Mathlib.Tactic.CC.or_eq_of_eq_false_left {a b : Prop} (h : a = False) :
(a ∨ b) = b
source
theorem Mathlib.Tactic.CC.or_eq_of_eq_false_right {a b : Prop} (h : b = False) :
(a ∨ b) = a
source
theorem Mathlib.Tactic.CC.or_eq_of_eq {a b : Prop} (h : a = b) :
(a ∨ b) = a
source
theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_left {a b : Prop} (h : a = True) :
(a → b) = b
source
theorem Mathlib.Tactic.CC.imp_eq_of_eq_true_right {a b : Prop} (h : b = True) :
(a → b) = True
source
theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_left {a b : Prop} (h : a = False) :
(a → b) = True
source
theorem Mathlib.Tactic.CC.imp_eq_of_eq_false_right {a b : Prop} (h : b = False) :
(a → b) = ¬a
source
theorem Mathlib.Tactic.CC.not_imp_eq_of_eq_false_right {a b : Prop} (h : b = False) :
(¬a → b) = a
source
theorem Mathlib.Tactic.CC.imp_eq_true_of_eq {a b : Prop} (h : a = b) :
(a → b) = True
source
theorem Mathlib.Tactic.CC.not_eq_of_eq_true {a : Prop} (h : a = True) :
(¬a) = False
source
theorem Mathlib.Tactic.CC.not_eq_of_eq_false {a : Prop} (h : a = False) :
(¬a) = True
source
theorem Mathlib.Tactic.CC.false_of_a_eq_not_a {a : Prop} (h : a = ¬a) :
False
source
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
source
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
source
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
source
theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_left {a b : Prop} (h : (a ∧ b) = True) :
a = True
source
theorem Mathlib.Tactic.CC.eq_true_of_and_eq_true_right {a b : Prop} (h : (a ∧ b) = True) :
b = True
source
theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_left {a b : Prop} (h : (a ∨ b) = False) :
a = False
source
theorem Mathlib.Tactic.CC.eq_false_of_or_eq_false_right {a b : Prop} (h : (a ∨ b) = False) :
b = False
source
theorem Mathlib.Tactic.CC.eq_false_of_not_eq_true {a : Prop} (h : (¬a) = True) :
a = False
source
theorem Mathlib.Tactic.CC.eq_true_of_not_eq_false {a : Prop} (h : (¬a) = False) :
a = True