-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearDisjoint (hypothesis)
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 (β := S) (⇑f : (a : S) → T) (⇑(M.mulMap N) : (a : ↥M ⊗[R] ↥N) → S))
⊢ 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 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)))
Tactic: rw [← coe_mulMap_comp_eq] at this
Cleared hypotheses: this