feat(Geometry/Euclidean/Projection): orthogonalProjectionSpan_congr (#31055)

Add a congruence lemma for `orthogonalProjectionSpan` applied to two simplices with the same set of vertices, analogous to and proved using `orthogonalProjection_congr`, and a variant
`orthogonalProjectionSpan_reindex`.

Author: jsm28

Mathlib/Geometry/Euclidean/Projection.lean

@@ -608,6 +608,16 @@ def orthogonalProjectionSpan {n : ℕ} (s : Simplex ℝ P n) :
     P →ᴬ[ℝ] affineSpan ℝ (Set.range s.points) :=
   orthogonalProjection (affineSpan ℝ (Set.range s.points))
 
+lemma orthogonalProjectionSpan_congr {m n : ℕ} {s₁ : Simplex ℝ P m} {s₂ : Simplex ℝ P n}
+    {p₁ p₂ : P} (h : Set.range s₁.points = Set.range s₂.points) (hp : p₁ = p₂) :
+    (s₁.orthogonalProjectionSpan p₁ : P) = s₂.orthogonalProjectionSpan p₂ :=
+  orthogonalProjection_congr (by rw [h]) hp
+
+@[simp] lemma orthogonalProjectionSpan_reindex {m n : ℕ} (s : Simplex ℝ P m)
+    (e : Fin (m + 1) ≃ Fin (n + 1)) (p : P) :
+    ((s.reindex e).orthogonalProjectionSpan p : P) = s.orthogonalProjectionSpan p :=
+  orthogonalProjectionSpan_congr (s.reindex_range_points e) rfl
+
 /-- Adding a vector to a point in the given subspace, then taking the
 orthogonal projection, produces the original point if the vector is a
 multiple of the result of subtracting a point's orthogonal projection