feat: add a congruence lemma for orthogonalProjection (#25004)

While it is still tricky to rewrite with `rw`, this makes it work with `simp`.

Author: eric-wieser

Mathlib/Geometry/Euclidean/Projection.lean

@@ -138,6 +138,20 @@ theorem orthogonalProjectionFn_eq {s : AffineSubspace ℝ P} [Nonempty s]
     orthogonalProjectionFn s p = orthogonalProjection s p :=
   rfl
 
+/-- Since both instance arguments are propositions, allow `simp` to rewrite them
+alongside the `s` argument.
+
+Note that without the coercion to `P`, the LHS and RHS would have different types. -/
+@[congr]
+theorem orthogonalProjection_congr {s₁ s₂ : AffineSubspace ℝ P} {p₁ p₂ : P}
+    [Nonempty s₁] [s₁.direction.HasOrthogonalProjection]
+    (h : s₁ = s₂) (hp : p₁ = p₂) :
+    letI : Nonempty s₂ := h ▸ ‹_›
+    letI : s₂.direction.HasOrthogonalProjection := h ▸ ‹_›
+    (orthogonalProjection s₁ p₁ : P) = (orthogonalProjection s₂ p₂ : P) := by
+  subst h hp
+  rfl
+
 /-- The linear map corresponding to `orthogonalProjection`. -/
 @[simp]
 theorem orthogonalProjection_linear {s : AffineSubspace ℝ P} [Nonempty s]