Commit 2022-11-06 08:14 aff50f9d

View on Github →

feat: port init/cc_lemmas.lean (#532) I started porting logic/lemmas.lean, but found that I needed cc_lemmas.lean first. Compare to

the Lean 3 version: https://github.com/leanprover-community/lean/blob/fc13c8c72a15dab71a2c2b31410c2cadc3526bd7/library/init/cc_lemmas.lean
the lean3port version: https://github.com/leanprover-community/lean/blob/fc13c8c72a15dab71a2c2b31410c2cadc3526bd7/library/init/cc_lemmas.lean The main adjustments I needed to make were of the form (true_iff_iff _) -> true_iff_iff, because the mathlib4 version of true_iff_iff (and similar lemmas) takes its argument implicitly, which the mathlib3 version takes it explicitly.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Init/CcLemmas.lean

added theorem and_eq_of_eq

added theorem and_eq_of_eq_false_left

added theorem and_eq_of_eq_false_right

added theorem and_eq_of_eq_true_left

added theorem and_eq_of_eq_true_right

added theorem eq_false_of_not_eq_true

added theorem eq_false_of_or_eq_false_left

added theorem eq_false_of_or_eq_false_right

added theorem eq_true_of_and_eq_true_left

added theorem eq_true_of_and_eq_true_right

added theorem eq_true_of_not_eq_false

added theorem false_of_a_eq_not_a

added theorem if_eq_of_eq

added theorem if_eq_of_eq_false

added theorem if_eq_of_eq_true

added theorem iff_eq_of_eq_true_left

added theorem iff_eq_of_eq_true_right

added theorem iff_eq_true_of_eq

added theorem imp_eq_of_eq_false_left

added theorem imp_eq_of_eq_false_right

added theorem imp_eq_of_eq_true_left

added theorem imp_eq_of_eq_true_right

added theorem imp_eq_true_of_eq

added theorem ne_of_eq_of_ne

added theorem ne_of_ne_of_eq

added theorem not_eq_of_eq_false

added theorem not_eq_of_eq_true

added theorem not_imp_eq_of_eq_false_right

added theorem or_eq_of_eq

added theorem or_eq_of_eq_false_left

added theorem or_eq_of_eq_false_right

added theorem or_eq_of_eq_true_left

added theorem or_eq_of_eq_true_right