Commit 2025-07-05 12:03 9ed286c0

View on Github →

style: replace HEq x y with x ≍ y (#26775) The notation ≍ for HEq was introduced in leanprover/lean4#8503 and all instances of HEq x y in core and Batteries are replaced with x ≍ y in leanprover/lean4#8872 and leanprover-community/batteries#1298. This PR applies the same replacement in Mathlib.

Estimated changes

modified theorem Composition.cast_heq
modified theorem Fin.val_eq_val_of_heq
modified theorem eq_cast_iff_heq
modified theorem heq_of_eq_cast
modified theorem Equiv.cast_eq_iff_heq
modified def foo
modified theorem ex14
modified theorem ex8