Commit 2025-05-19 11:40 9c644b13
View on Github →refactor(Geometry/Euclidean): use the simp-normal form in lemmas (#24996)
This replaces s.points '' ↑(univ.erase i) and (Set.range (s.faceOpposite i).points) with s.points '' {i}ᶜ, which makes more lemmas possible to tag with simp.