# Documentation

Mathlib.Init.CcLemmas

Lemmas use by the congruence closure module

theorem iff_eq_of_eq_true_left {a : Prop} {b : Prop} (h : ) :
(a b) = b
theorem iff_eq_of_eq_true_right {a : Prop} {b : Prop} (h : ) :
(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 b) = b
theorem and_eq_of_eq_true_right {a : Prop} {b : Prop} (h : ) :
(a b) = a
theorem and_eq_of_eq_false_left {a : Prop} {b : Prop} (h : ) :
(a b) = False
theorem and_eq_of_eq_false_right {a : Prop} {b : Prop} (h : ) :
(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 b) = True
theorem or_eq_of_eq_true_right {a : Prop} {b : Prop} (h : ) :
(a b) = True
theorem or_eq_of_eq_false_left {a : Prop} {b : Prop} (h : ) :
(a b) = b
theorem or_eq_of_eq_false_right {a : Prop} {b : Prop} (h : ) :
(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 : ) :
(ab) = b
theorem imp_eq_of_eq_true_right {a : Prop} {b : Prop} (h : ) :
(ab) = True
theorem imp_eq_of_eq_false_left {a : Prop} {b : Prop} (h : ) :
(ab) = True
theorem imp_eq_of_eq_false_right {a : Prop} {b : Prop} (h : ) :
(ab) = ¬a
theorem not_imp_eq_of_eq_false_right {a : Prop} {b : Prop} (h : ) :
(¬ab) = a
theorem imp_eq_true_of_eq {a : Prop} {b : Prop} (h : a = b) :
(ab) = True
theorem not_eq_of_eq_true {a : Prop} (h : ) :
theorem not_eq_of_eq_false {a : Prop} (h : ) :
(¬a) = True
theorem false_of_a_eq_not_a {a : Prop} (h : a = ¬a) :
theorem if_eq_of_eq_true {c : Prop} [d : ] {α : Sort u} (t : α) (e : α) (h : ) :
(if c then t else e) = t
theorem if_eq_of_eq_false {c : Prop} [d : ] {α : Sort u} (t : α) (e : α) (h : ) :
(if c then t else e) = e
theorem if_eq_of_eq (c : Prop) [d : ] {α : 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) :
theorem eq_true_of_and_eq_true_right {a : Prop} {b : Prop} (h : (a b) = True) :
theorem eq_false_of_or_eq_false_left {a : Prop} {b : Prop} (h : (a b) = False) :
theorem eq_false_of_or_eq_false_right {a : Prop} {b : Prop} (h : (a b) = False) :
theorem eq_false_of_not_eq_true {a : Prop} (h : (¬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.