Commit 2024-02-20 23:51 91c04061

View on Github →

chore: Remove Init.CCLemmas (#10696) Those lemmas were weird and unused, except the last few about transitivity of = and ≠, which I moved to Logic.Basic

Estimated changes

deleted theorem and_eq_of_eq
deleted theorem and_eq_of_eq_false_left
deleted theorem and_eq_of_eq_false_right
deleted theorem and_eq_of_eq_true_left
deleted theorem and_eq_of_eq_true_right
deleted theorem eq_false_of_not_eq_true
deleted theorem eq_true_of_not_eq_false
deleted theorem false_of_a_eq_not_a
deleted theorem if_eq_of_eq
deleted theorem if_eq_of_eq_false
deleted theorem if_eq_of_eq_true
deleted theorem iff_eq_of_eq_true_left
deleted theorem iff_eq_of_eq_true_right
deleted theorem iff_eq_true_of_eq
deleted theorem imp_eq_of_eq_false_left
deleted theorem imp_eq_of_eq_false_right
deleted theorem imp_eq_of_eq_true_left
deleted theorem imp_eq_of_eq_true_right
deleted theorem imp_eq_true_of_eq
deleted theorem ne_of_eq_of_ne
deleted theorem ne_of_ne_of_eq
deleted theorem not_eq_of_eq_false
deleted theorem not_eq_of_eq_true
deleted theorem or_eq_of_eq
deleted theorem or_eq_of_eq_false_left
deleted theorem or_eq_of_eq_false_right
deleted theorem or_eq_of_eq_true_left
deleted theorem or_eq_of_eq_true_right
added theorem ne_of_eq_of_ne
added theorem ne_of_ne_of_eq