-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (goal)
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
H : Function.Injective (α := ↥M ⊗[R] ↥N) (β := S) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S)
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective.{v + 1, w + 1} (α := S) (β := T) (⇑f : (a : S) → T)
this :
  Function.Injective.{v + 1, w + 1} (α := ↥M ⊗[R] ↥N) (β := T)
    (Function.comp (β :=
      ↥(Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            M) ⊗[R]
        ↥(Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            N))
      (⇑(mulMap
            (Submodule.map (σ₁₂ := RingHom.id R)
              (↑f :
                [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
              M)
            (Submodule.map (σ₁₂ := RingHom.id R)
              (↑f :
                [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
              N)) :
        (a :
            ↥(Submodule.map
                  (↑f :
                    [inst_5 : FunLike (S →ₐ[R] T) S T] →
                      [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                  M) ⊗[R]
              ↥(Submodule.map
                  (↑f :
                    [inst_5 : FunLike (S →ₐ[R] T) S T] →
                      [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                  N)) →
          T)
      (⇑(TensorProduct.map
            (LinearMap.submoduleMap
              (↑f :
                [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
              M)
            (LinearMap.submoduleMap
              (↑f :
                [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
              N)) :
        (a : ↥M ⊗[R] ↥N) →
          ↥(Submodule.map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M) ⊗[R]
            ↥(Submodule.map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                N)))
⊢ Function.Injective.{w + 1, w + 1} (α :=
    ↥(Submodule.map (σ₁₂ := RingHom.id R)
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          M) ⊗[R]
      ↥(Submodule.map (σ₁₂ := RingHom.id R)
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          N))
    (β := T)
    (⇑(mulMap
          (Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            M)
          (Submodule.map (σ₁₂ := RingHom.id R)
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            N)) :
      (a :
          ↥(Submodule.map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M) ⊗[R]
            ↥(Submodule.map
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                N)) →
        T)
have refine : Function.Surjective.{v + 1, w + 1} (α := ↥M ⊗[R] ↥N) (β :=
  ↥(Submodule.map (σ₁₂ := RingHom.id R)
        (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
        M) ⊗[R]
    ↥(Submodule.map (σ₁₂ := RingHom.id R)
        (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) N))
  (⇑(TensorProduct.map
        (LinearMap.submoduleMap
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) M)
        (LinearMap.submoduleMap
          (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
          N)) :
    (a : ↥M ⊗[R] ↥N) →
      ↥(Submodule.map
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            M) ⊗[R]
        ↥(Submodule.map
            (↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
            N))
Tactic: refine this.of_comp_right ?_