refactor(Geometry/Euclidean): use orthogonalProjectionSpan more (#24503)

Make more use of `orthogonalProjectionSpan` in
`Mathlib.Geometry.Euclidean.Projection` and
`Mathlib.Geometry.Euclidean.SignedDist`.  Split out from #23752.

Author: jsm28

Mathlib/Geometry/Euclidean/Projection.lean

@@ -567,16 +567,14 @@ theorem dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq
 variable {n : ℕ} [NeZero n] (s : Simplex ℝ P n)
 
 @[simp] lemma ne_orthogonalProjection_faceOpposite (i : Fin (n + 1)) :
-    s.points i ≠
-      orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i) := by
+    s.points i ≠ (s.faceOpposite i).orthogonalProjectionSpan (s.points i) := by
   intro h
-  rw [eq_comm, EuclideanGeometry.orthogonalProjection_eq_self_iff,
+  rw [eq_comm, orthogonalProjectionSpan, EuclideanGeometry.orthogonalProjection_eq_self_iff,
     mem_affineSpan_range_faceOpposite_points_iff] at h
   simp at h
 
 lemma dist_orthogonalProjection_faceOpposite_pos (i : Fin (n + 1)) :
-    0 < dist (s.points i)
-      (orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)) := by
+    0 < dist (s.points i) ((s.faceOpposite i).orthogonalProjectionSpan (s.points i)) := by
   simp
 
 end Simplex

Mathlib/Geometry/Euclidean/SignedDist.lean

@@ -98,7 +98,7 @@ noncomputable def signedInfDist : P →ᵃ[ℝ] ℝ :=
   AffineSubspace.signedInfDist (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)
 
 lemma signedInfDist_apply_self : s.signedInfDist i (s.points i) = ‖s.points i -ᵥ
-    orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)‖ :=
+    (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖ :=
   AffineSubspace.signedInfDist_apply_self _ _
 
 variable {i} in
@@ -108,11 +108,10 @@ lemma signedInfDist_apply_of_ne {j : Fin (n + 1)} (h : j ≠ i) :
 
 lemma signedInfDist_affineCombination {w : Fin (n + 1) → ℝ} (h : ∑ i, w i = 1) :
     s.signedInfDist i (Finset.univ.affineCombination ℝ s.points w) = w i * ‖s.points i -ᵥ
-      orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)‖ := by
+      (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖ := by
   rw [Finset.map_affineCombination _ _ _ h,
     Finset.univ.affineCombination_apply_eq_lineMap_sum w (s.signedInfDist i ∘ s.points) 0
-      ‖s.points i -ᵥ
-       orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.points i)‖
+      ‖s.points i -ᵥ (s.faceOpposite i).orthogonalProjectionSpan (s.points i)‖
       {i} h]
   · simp [AffineMap.lineMap_apply]
   · simp [signedInfDist_apply_self]
@@ -125,7 +124,7 @@ variable {s} in
 lemma abs_signedInfDist_eq_dist_of_mem_affineSpan_range {p : P}
     (h : p ∈ affineSpan ℝ (Set.range s.points)) :
     |s.signedInfDist i p| =
-      dist p (orthogonalProjection (affineSpan ℝ (Set.range (s.faceOpposite i).points)) p) := by
+      dist p ((s.faceOpposite i).orthogonalProjectionSpan p) := by
   apply AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert
   rw [affineSpan_insert_affineSpan]
   convert h