mathlib3

847f87ee - feat(geometry/euclidean/circumcenter): lemmas on orthogonal projection and reflection (#4087)

feat(geometry/euclidean/circumcenter): lemmas on orthogonal projection and reflection (#4087) Add more lemmas about orthogonal projection and the circumcenter of a simplex (so substantially simplifying the proof of `orthogonal_projection_circumcenter`). Then prove a lemma `eq_or_eq_reflection_of_dist_eq` that if we fix a distance a point has to all the vertices of a simplex, any two possible positions of that point in one dimension higher than the simplex are equal or reflections of each other in the subspace of the simplex.