feat(Geometry/Euclidean/Projection): characteristic property (#30698)

Add a lemma

```lean
lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
    [s.direction.HasOrthogonalProjection] {p q : P} :
    orthogonalProjection s p = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ := by
```

that gives the characteristic property of the orthogonal projection in a more convenient form to use than the existing
`inter_eq_singleton_orthogonalProjection` (from which it is derived).

Deduce a lemma `orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem` about equality of two projections onto the same subspace.

Author: jsm28

Mathlib/Geometry/Euclidean/Projection.lean

@@ -276,6 +276,40 @@ theorem orthogonalProjection_vsub_orthogonalProjection (s : AffineSubspace ℝ P
   rw [← neg_vsub_eq_vsub_rev, inner_neg_right,
     orthogonalProjection_vsub_mem_direction_orthogonal s p c hc, neg_zero]
 
+/-- The characteristic property of the orthogonal projection, for a point given in the underlying
+space. This form is typically more convenient to use than
+`inter_eq_singleton_orthogonalProjection`. -/
+lemma coe_orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
+    [s.direction.HasOrthogonalProjection] {p q : P} :
+    orthogonalProjection s p = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ := by
+  constructor
+  · rintro rfl
+    exact ⟨orthogonalProjection_mem _, vsub_orthogonalProjection_mem_direction_orthogonal _ _⟩
+  · rintro ⟨hqs, hpq⟩
+    have hq : q ∈ mk' p s.directionᗮ := by
+      rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
+    suffices q ∈ ({(orthogonalProjection s p : P)} : Set P) by
+      simpa [eq_comm] using this
+    rw [← inter_eq_singleton_orthogonalProjection]
+    simp only [Set.mem_inter_iff, SetLike.mem_coe]
+    exact ⟨hqs, hq⟩
+
+/-- The characteristic property of the orthogonal projection, for a point given in the relevant
+subspace. This form is typically more convenient to use than
+`inter_eq_singleton_orthogonalProjection`. -/
+lemma orthogonalProjection_eq_iff_mem {s : AffineSubspace ℝ P} [Nonempty s]
+    [s.direction.HasOrthogonalProjection] {p : P} {q : s} :
+    orthogonalProjection s p = q ↔ p -ᵥ q ∈ s.directionᗮ := by
+  simpa using coe_orthogonalProjection_eq_iff_mem (s := s) (p := p) (q := (q : P))
+
+/-- A condition for two points to have the same orthogonal projection onto a given subspace. -/
+lemma orthogonalProjection_eq_orthogonalProjection_iff_vsub_mem {s : AffineSubspace ℝ P}
+    [Nonempty s] [s.direction.HasOrthogonalProjection] {p q : P} :
+    orthogonalProjection s p = orthogonalProjection s q ↔ p -ᵥ q ∈ s.directionᗮ := by
+  rw [orthogonalProjection_eq_iff_mem, ← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q)
+    (vsub_orthogonalProjection_mem_direction_orthogonal s q)]
+  simp
+
 /-- Adding a vector to a point in the given subspace, then taking the
 orthogonal projection, produces the original point if the vector was
 in the orthogonal direction. -/