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.
