chore(Analysis/InnerProductSpace/Projection/Submodule): rename lemmas (#33337)

Author: themathqueen

Mathlib/Analysis/InnerProductSpace/Positive.lean

@@ -242,7 +242,7 @@ theorem IsSymmetricProjection.le_iff_range_le_range {p q : E →ₗ[𝕜] E}
   simp_rw [sub_apply, inner_sub_left, map_sub, hh hq, hh hp,
     hp.isIdempotentElem.mem_range_iff.mp ha, sub_nonneg, sq_le_sq, abs_norm] at h2
   obtain ⟨U, _, rfl⟩ := isSymmetricProjection_iff_eq_coe_starProjection.mp hq
-  simpa [Submodule.starProjection_coe_eq_isCompl_projection] using
+  simpa [Submodule.toLinearMap_starProjection_eq_isComplProjection] using
     U.mem_iff_norm_starProjection _ |>.mpr <| le_antisymm (U.norm_starProjection_apply_le a) h2
 
 end LinearMap
@@ -501,7 +501,7 @@ theorem Submodule.starProjection_le_starProjection_iff {U V : Submodule 𝕜 E}
     U.starProjection ≤ V.starProjection ↔ U ≤ V := by
   simp_rw [← coe_le_coe_iff, isSymmetricProjection_starProjection _
       |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _,
-    starProjection_coe_eq_isCompl_projection, IsCompl.projection_range]
+    toLinearMap_starProjection_eq_isComplProjection, IsCompl.projection_range]
 
 /-- `U.starProjection = V.starProjection` iff `U = V`. -/
 theorem Submodule.starProjection_inj {U V : Submodule 𝕜 E}

Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

@@ -181,7 +181,7 @@ theorem topologicalClosure_eq_top_iff [CompleteSpace E] :
   · rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]
   · rw [h, Submodule.bot_orthogonal_eq_top]
 
-theorem orthogonalProjection_eq_linearProjOfIsCompl [K.HasOrthogonalProjection] (x : E) :
+theorem orthogonalProjection_apply_eq_linearProjOfIsCompl [K.HasOrthogonalProjection] (x : E) :
     K.orthogonalProjection x =
       K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection x := by
   have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
@@ -191,20 +191,27 @@ theorem orthogonalProjection_eq_linearProjOfIsCompl [K.HasOrthogonalProjection]
     orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
 
 @[deprecated (since := "2025-07-11")] alias orthogonalProjection_eq_linear_proj :=
-  orthogonalProjection_eq_linearProjOfIsCompl
+  orthogonalProjection_apply_eq_linearProjOfIsCompl
+@[deprecated (since := "2025-12-26")] alias orthogonalProjection_eq_linearProjOfIsCompl :=
+  orthogonalProjection_apply_eq_linearProjOfIsCompl
 
-theorem orthogonalProjection_coe_eq_linearProjOfIsCompl [K.HasOrthogonalProjection] :
+theorem toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl [K.HasOrthogonalProjection] :
     (K.orthogonalProjection : E →ₗ[𝕜] K) =
       K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection :=
-  LinearMap.ext <| orthogonalProjection_eq_linearProjOfIsCompl
+  LinearMap.ext orthogonalProjection_apply_eq_linearProjOfIsCompl
 
 @[deprecated (since := "2025-07-11")] alias orthogonalProjection_coe_linearMap_eq_linearProj :=
-  orthogonalProjection_coe_eq_linearProjOfIsCompl
+  toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl
+@[deprecated (since := "2025-12-26")] alias orthogonalProjection_coe_eq_linearProjOfIsCompl :=
+  toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl
 
 open Submodule in
-theorem starProjection_coe_eq_isCompl_projection [K.HasOrthogonalProjection] :
+theorem toLinearMap_starProjection_eq_isComplProjection [K.HasOrthogonalProjection] :
     K.starProjection.toLinearMap = K.isCompl_orthogonal_of_hasOrthogonalProjection.projection := by
-  simp [starProjection, orthogonalProjection_coe_eq_linearProjOfIsCompl, IsCompl.projection]
+  simp [starProjection, toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, IsCompl.projection]
+
+@[deprecated (since := "2025-12-26")] alias starProjection_coe_eq_isCompl_projection :=
+  toLinearMap_starProjection_eq_isComplProjection
 
 end Submodule