mathlib documentation

core.init.cc_lemmas

theorem iff_eq_of_eq_true_left {a b : Prop} :
a = true(a b) = b

theorem iff_eq_of_eq_true_right {a b : Prop} :
b = true(a b) = a

theorem iff_eq_true_of_eq {a b : Prop} :
a = b(a b) = true

theorem and_eq_of_eq_true_left {a b : Prop} :
a = true(a b) = b

theorem and_eq_of_eq_true_right {a b : Prop} :
b = true(a b) = a

theorem and_eq_of_eq_false_left {a b : Prop} :
a = false(a b) = false

theorem and_eq_of_eq_false_right {a b : Prop} :
b = false(a b) = false

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

theorem or_eq_of_eq_true_left {a b : Prop} :
a = true(a b) = true

theorem or_eq_of_eq_true_right {a b : Prop} :
b = true(a b) = true

theorem or_eq_of_eq_false_left {a b : Prop} :
a = false(a b) = b

theorem or_eq_of_eq_false_right {a b : Prop} :
b = false(a b) = a

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

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

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

theorem imp_eq_of_eq_false_left {a b : Prop} :
a = false(a → b) = true

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

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

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

theorem not_eq_of_eq_true {a : Prop} :
a = true(¬a) = false

theorem not_eq_of_eq_false {a : Prop} :
a = false(¬a) = true

theorem false_of_a_eq_not_a {a : Prop} :
a = ¬afalse

theorem if_eq_of_eq_true {c : Prop} [d : decidable c] {α : Sort u} (t e : α) :
c = trueite c t e = t

theorem if_eq_of_eq_false {c : Prop} [d : decidable c] {α : Sort u} (t e : α) :
c = falseite c t e = e

theorem if_eq_of_eq (c : Prop) [d : decidable c] {α : Sort u} {t e : α} :
t = eite c t e = t

theorem eq_true_of_and_eq_true_left {a b : Prop} :
(a b) = truea = true

theorem eq_true_of_and_eq_true_right {a b : Prop} :
(a b) = trueb = true

theorem eq_false_of_or_eq_false_left {a b : Prop} :
(a b) = falsea = false

theorem eq_false_of_or_eq_false_right {a b : Prop} :
(a b) = falseb = false

theorem eq_false_of_not_eq_true {a : Prop} :
(¬a) = truea = false

theorem eq_true_of_not_eq_false {a : Prop} :
(¬a) = falsea = true

theorem ne_of_eq_of_ne {α : Sort u} {a b c : α} :
a = bb ca c

theorem ne_of_ne_of_eq {α : Sort u} {a b c : α} :
a bb = ca c