# Commit 2022-02-24 11:57 b8b1b578

View on Github →chore(geometry/euclidean): split repetitive proof (#12209)
This PR is part of the subobject refactor #11545, fixing a timeout caused by some expensive defeq checks.
I introduce a new definition `simplex.orthogonal_projection_span s := orthogonal_projection (affine_span ℝ (set.range s.points))`

, and extract a couple of its properties from (repetitive) parts of proofs in `circumcenter.lean`

, especially `eq_or_eq_reflection_of_dist_eq`

. This makes the latter proof noticeably faster, especially after commit #11750.