Commit 2025-11-24 11:02 a37790b6
View on Github →chore: cleanup of some cast lemmas (#31933)
Remove some unused simp annotations on cast lemmas, and reverse the direction of two Equiv.cast lemmas, to push casts inwards rather than outwards. c.f. #31575