feat(geometry/euclidean/angle/oriented/affine): equidistant points an…

…d `π / 2` rotations (#17722)

Add the following lemma: two different points are equidistant from a third point if and only if that third point equals some multiple of a `π / 2` rotation of the vector between those points, plus the midpoint of those points.  In particular, this is useful for bisecting an isosceles triangle then applying trigonometric lemmas about right-angled triangles from #17683 to the result.

src/geometry/euclidean/angle/oriented/affine.lean

@@ -538,6 +538,34 @@ lemma _root_.collinear.two_zsmul_oangle_eq_right {p₁ p₂ p₃ p₃' : P}
   (2 : ℤ) • ∡ p₁ p₂ p₃ = (2 : ℤ) • ∡ p₁ p₂ p₃' :=
 by rw [oangle_rev, smul_neg, h.two_zsmul_oangle_eq_left hp₃p₂ hp₃'p₂, ←smul_neg, ←oangle_rev]
 
+/-- Two different points are equidistant from a third point if and only if that third point
+equals some multiple of a `π / 2` rotation of the vector between those points, plus the midpoint
+of those points. -/
+lemma dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint {p₁ p₂ p : P} (h : p₁ ≠ p₂) :
+  dist p₁ p = dist p₂ p ↔
+    ∃ r : ℝ, r • ((o).rotation (π / 2 : ℝ) (p₂ -ᵥ p₁)) +ᵥ midpoint ℝ p₁ p₂ = p :=
+begin
+  refine ⟨λ hd, _, λ hr, _⟩,
+  { have hi : ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0,
+    { rw [@dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V,
+          ←mul_self_inj (norm_nonneg _) (norm_nonneg _), ←real_inner_self_eq_norm_mul_norm,
+          ←real_inner_self_eq_norm_mul_norm] at hd,
+      simp_rw [vsub_midpoint, ←vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, 
+               inner_add_right, inner_smul_right, hd, real_inner_comm (p -ᵥ p₁)],
+      abel },
+    rw [@orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two V _ _ o,
+        or_iff_right (vsub_ne_zero.2 h.symm)] at hi,
+    rcases hi with ⟨r, hr⟩,
+    rw [eq_comm, ←eq_vadd_iff_vsub_eq] at hr,
+    exact ⟨r, hr.symm⟩ },
+  { rcases hr with ⟨r, rfl⟩,
+    simp_rw [@dist_eq_norm_vsub V, vsub_vadd_eq_vsub_sub, left_vsub_midpoint,
+             right_vsub_midpoint, inv_of_eq_inv, ←neg_vsub_eq_vsub_rev p₂ p₁,
+             ←mul_self_inj (norm_nonneg _) (norm_nonneg _), ←real_inner_self_eq_norm_mul_norm,
+             inner_sub_sub_self],
+    simp [-neg_vsub_eq_vsub_rev] }
+end
+
 open affine_subspace
 
 /-- Given two pairs of distinct points on the same line, such that the vectors between those