chore(LinearAlgebra/Projection): deprecating subtype ∘ linearProjOfIsCompl in favor of IsCompl.projection (leanprover-community#27644)

This deprecates all instances of `U.subtype ∘ U.linearProjOfIsCompl V hUV` and `(U.linearProjOfIsCompl V hUV x : E)` in favor of `hUV.projection` and `hUV.projection x` respectively in `LinearAlgebra/Projection` and other files.

Author: themathqueen

Mathlib/Algebra/Lie/LieTheorem.lean

@@ -180,14 +180,15 @@ theorem exists_nontrivial_weightSpace_of_lieIdeal [LieModule.IsTriangularizable
   refine nontrivial_of_ne ⟨v, ?_⟩ 0 ?_
   · rw [mem_weightSpace]
     intro x
-    have hπ : (π₁ x : L) + π₂ x = x := linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self hA x
-    suffices ⁅(π₂ x : L), v⁆ = (c • e (π₂ x)) • v by
+    have hπ : (π₁ x : L) + π₂ x = x := hA.projection_add_projection_eq_self x
+    suffices ⁅hA.symm.projection x, v⁆ = (c • e (π₂ x)) • v by
       calc ⁅x, v⁆
-          = ⁅π₁ x, v⁆       + ⁅(π₂ x : L), v⁆    := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
-        _ =  χ₀ (π₁ x) • v  + (c • e (π₂ x)) • v := by rw [hv' (π₁ x), this]
+          = ⁅π₁ x, v⁆       + ⁅hA.symm.projection x, v⁆ := congr(⁅$hπ.symm, v⁆) ▸ add_lie _ _ _
+        _ =  χ₀ (π₁ x) • v  + (c • e (π₂ x)) • v        := by rw [hv' (π₁ x), this]
         _ = _ := by simp [add_smul]
-    calc ⁅(π₂ x : L), v⁆
-        = e (π₂ x) • ↑(c • ⟨v, hv⟩ : W) := by rw [← he, smul_lie, ← hvc.apply_eq_smul]; rfl
+    calc ⁅hA.symm.projection x, v⁆
+        = e (π₂ x) • ↑(c • ⟨v, hv⟩ : W)   := by
+          rw [IsCompl.projection_apply, ← he, smul_lie, ← hvc.apply_eq_smul]; rfl
       _ = (c • e (π₂ x)) • v              := by rw [smul_assoc, smul_comm]; rfl
   · simpa [ne_eq, LieSubmodule.mk_eq_zero] using hvc.right
 

Mathlib/Analysis/InnerProductSpace/Projection/Submodule.lean

@@ -182,7 +182,8 @@ theorem orthogonalProjection_eq_linearProjOfIsCompl [K.HasOrthogonalProjection]
     K.orthogonalProjection x =
       K.linearProjOfIsCompl _ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection x := by
   have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
-  conv_lhs => rw [← Submodule.linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self this x]
+  conv_lhs => rw [← IsCompl.projection_add_projection_eq_self this x]
+  simp_rw [IsCompl.projection_apply]
   rw [map_add, orthogonalProjection_mem_subspace_eq_self,
     orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
 

Mathlib/Analysis/InnerProductSpace/Symmetric.lean

@@ -273,8 +273,8 @@ theorem _root_.Submodule.IsCompl.projection_isSymmetric_iff
       ← Submodule.linearProjOfIsCompl_apply_left hUV ⟨u, hu⟩, ← U.subtype_apply, ← comp_apply,
       ← h, comp_apply, linearProjOfIsCompl_apply_right hUV ⟨v, hv⟩,
       map_zero, inner_zero_left]
-  · nth_rw 2 [← linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self hUV x]
-    nth_rw 1 [← linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self hUV y]
+  · nth_rw 2 [← hUV.projection_add_projection_eq_self x]
+    nth_rw 1 [← hUV.projection_add_projection_eq_self y]
     rw [isOrtho_iff_inner_eq] at h
     simp [inner_add_right, inner_add_left, h, inner_eq_zero_symm]
 

Mathlib/LinearAlgebra/Projection.lean

@@ -156,10 +156,15 @@ theorem IsCompl.projection_apply (hpq : IsCompl p q) (x : E) :
     hpq.projection x = p.linearProjOfIsCompl q hpq x :=
   rfl
 
+@[simp]
+theorem coe_linearProjOfIsCompl_apply (hpq : IsCompl p q) (x : E) :
+    (p.linearProjOfIsCompl q hpq x : E) = hpq.projection x :=
+  rfl
+
 @[simp]
 theorem IsCompl.projection_apply_mem (hpq : IsCompl p q) (x : E) :
-    hpq.projection x ∈ p := by
-  simp [projection]
+    hpq.projection x ∈ p :=
+  SetLike.coe_mem _
 
 @[simp]
 theorem linearProjOfIsCompl_apply_left (h : IsCompl p q) (x : p) :
@@ -188,7 +193,7 @@ theorem linearProjOfIsCompl_apply_eq_zero_iff (h : IsCompl p q) {x : E} :
 @[simp]
 theorem IsCompl.projection_apply_eq_zero_iff (hpq : IsCompl p q) {x : E} :
     hpq.projection x = 0 ↔ x ∈ q := by
-  simp [projection, linearProjOfIsCompl_apply_eq_zero_iff hpq]
+  simp [projection, -coe_linearProjOfIsCompl_apply]
 
 theorem linearProjOfIsCompl_apply_right' (h : IsCompl p q) (x : E) (hx : x ∈ q) :
     linearProjOfIsCompl p q h x = 0 :=
@@ -212,14 +217,18 @@ theorem linearProjOfIsCompl_comp_subtype (h : IsCompl p q) :
     (linearProjOfIsCompl p q h).comp p.subtype = LinearMap.id :=
   LinearMap.ext <| linearProjOfIsCompl_apply_left h
 
-theorem linearProjOfIsCompl_idempotent (h : IsCompl p q) (x : E) :
-    linearProjOfIsCompl p q h (linearProjOfIsCompl p q h x) = linearProjOfIsCompl p q h x :=
+theorem linearProjOfIsCompl_isCompl_projection (h : IsCompl p q) (x : E) :
+    linearProjOfIsCompl p q h (h.projection x) = linearProjOfIsCompl p q h x :=
   linearProjOfIsCompl_apply_left h _
 
+@[deprecated (since := "2025-07-29")] alias linearProjOfIsCompl_idempotent :=
+  linearProjOfIsCompl_isCompl_projection
+
 /-- The linear projection onto a subspace along its complement is an idempotent. -/
+@[simp]
 theorem IsCompl.projection_isIdempotentElem (hpq : IsCompl p q) :
-    IsIdempotentElem hpq.projection := by
-  simp [projection, IsIdempotentElem, LinearMap.ext_iff]
+    IsIdempotentElem hpq.projection :=
+  LinearMap.ext fun _ ↦ congr($(linearProjOfIsCompl_isCompl_projection hpq _))
 
 theorem existsUnique_add_of_isCompl_prod (hc : IsCompl p q) (x : E) :
     ∃! u : p × q, (u.fst : E) + u.snd = x :=
@@ -230,28 +239,32 @@ theorem existsUnique_add_of_isCompl (hc : IsCompl p q) (x : E) :
   let ⟨u, hu₁, hu₂⟩ := existsUnique_add_of_isCompl_prod hc x
   ⟨u.1, u.2, hu₁, fun r s hrs => Prod.eq_iff_fst_eq_snd_eq.1 (hu₂ ⟨r, s⟩ hrs)⟩
 
-theorem linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self (hpq : IsCompl p q) (x : E) :
-    (p.linearProjOfIsCompl q hpq x + q.linearProjOfIsCompl p hpq.symm x : E) = x := by
-  dsimp only [linearProjOfIsCompl]
+theorem IsCompl.projection_add_projection_eq_self (hpq : IsCompl p q) (x : E) :
+    hpq.projection x + hpq.symm.projection x = x := by
+  dsimp only [IsCompl.projection, linearProjOfIsCompl]
   rw [← prodComm_trans_prodEquivOfIsCompl _ _ hpq]
   exact (prodEquivOfIsCompl _ _ hpq).apply_symm_apply x
 
+@[deprecated (since := "2025-07-29")] alias linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self :=
+  IsCompl.projection_add_projection_eq_self
+
 @[deprecated (since := "2025-07-11")] alias linear_proj_add_linearProjOfIsCompl_eq_self :=
   linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self
 
-lemma linearProjOfIsCompl_eq_self_sub_linearProjOfIsCompl (hpq : IsCompl p q) (x : E) :
-    (q.linearProjOfIsCompl p hpq.symm x : E) = x - (p.linearProjOfIsCompl q hpq x : E) := by
-  rw [eq_sub_iff_add_eq, linearProjOfIsCompl_add_linearProjOfIsCompl_eq_self]
+lemma IsCompl.projection_eq_self_sub_projection (hpq : IsCompl p q) (x : E) :
+    hpq.symm.projection x = x - hpq.projection x := by
+  rw [eq_sub_iff_add_eq, projection_add_projection_eq_self]
 
-/-- The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`. -/
-@[simp] lemma linearProjOfIsCompl_eq_self_iff (hpq : IsCompl p q) (x : E) :
-    (p.linearProjOfIsCompl q hpq x : E) = x ↔ x ∈ p := by
-  rw [eq_comm, ← sub_eq_zero, ← linearProjOfIsCompl_eq_self_sub_linearProjOfIsCompl,
-    coe_eq_zero, linearProjOfIsCompl_apply_eq_zero_iff]
+@[deprecated (since := "2025-07-29")] alias linearProjOfIsCompl_eq_self_sub_linearProjOfIsCompl :=
+  IsCompl.projection_eq_self_sub_projection
 
+/-- The projection to `p` along `q` of `x` equals `x` if and only if `x ∈ p`. -/
 @[simp] lemma IsCompl.projection_eq_self_iff (hpq : IsCompl p q) (x : E) :
     hpq.projection x = x ↔ x ∈ p := by
-  rw [hpq.projection_apply, linearProjOfIsCompl_eq_self_iff hpq]
+  rw [eq_comm, ← sub_eq_zero, ← projection_eq_self_sub_projection, projection_apply_eq_zero_iff]
+
+@[deprecated (since := "2025-07-29")] alias linearProjOfIsCompl_eq_self_iff :=
+  IsCompl.projection_eq_self_iff
 
 end Submodule
 
@@ -346,8 +359,8 @@ theorem range_ofIsCompl (hpq : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[
     all_goals rintro - ⟨x, rfl⟩; exact ⟨x, by simp⟩
 
 theorem ofIsCompl_subtype_zero_eq (hpq : IsCompl p q) :
-    ofIsCompl hpq p.subtype 0 = p.subtype ∘ₗ p.linearProjOfIsCompl q hpq := by
-  simp [ofIsCompl_eq_add]
+    ofIsCompl hpq p.subtype 0 = hpq.projection := by
+  simp [ofIsCompl_eq_add, IsCompl.projection]
 
 theorem ofIsCompl_symm (hpq : IsCompl p q) {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} :
     ofIsCompl hpq.symm ψ φ = ofIsCompl hpq φ ψ := by