feat(LinearAlgebra/Projection): add quotientEquivOfIsCompl_comp_mkQ and quotientEquivOfIsTopCompl_comp_mkQ (leanprover-community#39613)

Adds the lemmas `Submodule.quotientEquivOfIsCompl_comp_mkQ` and `quotientEquivOfIsTopCompl_comp_mkQ` - the composition of `quotientEquivOfIsCompl`/`quotientEquivOfIsTopCompl` with `mkQ` agrees with the linear projection onto `q`  along `p`. Additionally the proof of `IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl` is simplified.

Author: sharky564

Mathlib/LinearAlgebra/Projection.lean

@@ -286,6 +286,10 @@ def quotientEquivOfIsCompl (h : IsCompl p q) : (E ⧸ p) ≃ₗ[R] q :=
     (by ext; simp)
     (by ext; simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem])
 
+theorem quotientEquivOfIsCompl_comp_mkQ (h : IsCompl p q) :
+    (quotientEquivOfIsCompl p q h : E ⧸ p →ₗ[R] q) ∘ₗ p.mkQ = q.projectionOnto p h.symm :=
+  rfl
+
 @[simp]
 theorem quotientEquivOfIsCompl_apply_mk (h : IsCompl p q) (x : E) :
     quotientEquivOfIsCompl p q h (Quotient.mk x) = q.projectionOnto p h.symm x :=

Mathlib/Topology/Algebra/Module/Complement.lean

@@ -450,10 +450,8 @@ theorem prodEquivOfIsTopCompl_symm_apply (h : IsTopCompl p q) (x : M) :
 `Submodule.quotientEquivOfIsCompl` is continuous. -/
 theorem IsCompl.isTopCompl_iff_continuous_quotientEquivOfIsCompl (h : IsCompl p q) :
     IsTopCompl p q ↔ Continuous (p.quotientEquivOfIsCompl q h) := by
-  have hproj : ⇑(p.quotientEquivOfIsCompl q h) ∘ ⇑p.mkQ = ⇑(q.projectionOnto p h.symm) := by
-    funext; simp
-  rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
-    isTopCompl_comm]
+  rw [p.isQuotientMap_mkQL.continuous_iff, isTopCompl_comm]
+  exact h.symm.isTopCompl_iff_projectionOnto
 
 variable (p q) in
 /-- If two submodules are topological complements, then the linear equivalence
@@ -469,6 +467,10 @@ theorem toLinearEquiv_quotientEquivOfIsTopCompl (h : IsTopCompl p q) :
     (quotientEquivOfIsTopCompl p q h : (M ⧸ p) ≃ₗ[R] q) = p.quotientEquivOfIsCompl q h.isCompl :=
   rfl
 
+theorem quotientEquivOfIsTopCompl_comp_mkQL (h : IsTopCompl p q) :
+    (quotientEquivOfIsTopCompl p q h) ∘L p.mkQL = q.projectionOntoL p h.symm :=
+  rfl
+
 @[simp]
 theorem quotientEquivOfIsTopCompl_apply (h : IsTopCompl p q) (x : M ⧸ p) :
     quotientEquivOfIsTopCompl p q h x = p.quotientEquivOfIsCompl q h.isCompl x :=