Commit 2025-09-16 23:57 1129426e

View on Github →

chore: deprecate some duplicate HEq lemmas (#29711)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

Modified Mathlib/Data/Fintype/Quotient.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem Eq.rec_eq_cast

deleted theorem eqRec_heq'

deleted theorem heq_rec_iff_heq

deleted theorem rec_heq_iff_heq

Modified Mathlib/Logic/Equiv/Basic.lean

Modified Mathlib/Tactic/CC/Addition.lean