Add surjective_linearMapComp_left_of_exists_rightInverse

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -511,6 +511,15 @@ lemma _root_.Function.Injective.injective_linearMapComp_left (hf : Injective f)
     Injective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g :=
   fun g₁ g₂ (h : f.comp g₁ = f.comp g₂) ↦ ext fun x ↦ hf <| by rw [← comp_apply, h, comp_apply]
 
+theorem surjective_linearMapComp_left_of_exists_rightInverse {σ₃₂ : R₃ →+* R₂}
+    [RingHomInvPair σ₂₃ σ₃₂] [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂]
+    (hf : ∃ f' : M₃ →ₛₗ[σ₃₂] M₂, f.comp f' = .id) :
+    Surjective fun g : M₁ →ₛₗ[σ₁₂] M₂ ↦ f.comp g := by
+  intro h
+  obtain ⟨f' ,hf'⟩ := hf
+  refine ⟨f'.comp h, ?_⟩
+  simp_rw [← comp_assoc, hf', id_comp]
+
 @[simp]
 theorem cancel_left (hf : Injective f) : f.comp g = f.comp g' ↔ g = g' :=
   hf.injective_linearMapComp_left.eq_iff

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -362,14 +362,10 @@ theorem injective_compr₂_of_injective (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g
     (hg : Injective g) : Injective (f.compr₂ g) :=
   hg.injective_linearMapComp_left.comp hf
 
+/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
 theorem surjective_compr₂_of_exists_rightInverse (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ)
     (hf : Surjective f) (hg : ∃ g' : Qₗ →ₗ[R] Pₗ, g.comp g' = LinearMap.id) :
-    Surjective (f.compr₂ g) := by
-  suffices Surjective (g.comp ·) from this.comp hf
-  intro h
-  obtain ⟨g', hg'⟩ := hg
-  refine ⟨g'.comp h, ?_⟩
-  simp_rw [← comp_assoc, hg', id_comp]
+    Surjective (f.compr₂ g) := (surjective_linearMapComp_left_of_exists_rightInverse hg).comp hf
 
 /-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map. -/
 theorem surjective_compr₂_of_equiv (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ ≃ₗ[R] Qₗ) (hf : Surjective f) :