refactor(geometry/euclidean): shorten proof (#6121)
... of `eq_reflection_of_eq_subspace`
Co-authors: `lean-gptf`, Stanislas Polu
This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data.
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
