-- Module: Mathlib.LinearAlgebra.TensorProduct.Submodule
Goal:
R : Type u
S : Type v
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M N : Submodule R S
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
a :
  ∀ (x : ↥M) (x_1 : ↥N),
    Eq.{w + 1} (α := T)
      (((((TensorProduct.AlgebraTensorModule.curry
                      (mulMap
                          (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)
                          (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)) :
                    ↥M →ₗ[R] LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
                  (a : ↥M) → ↥N →ₗ[R] T)
                x :
              LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
            (a : ↥N) → T)
          x_1 :
        T)
      (((((TensorProduct.AlgebraTensorModule.curry
                      ((↑f :
                          [inst_5 : FunLike (S →ₐ[R] T) S T] →
                            [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) ∘ₗ
                        M.mulMap N) :
                    ↥M →ₗ[R] LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
                  (a : ↥M) → ↥N →ₗ[R] T)
                x :
              LinearMap.{u, u, v, w} (RingHom.id R) (↥N) T) :
            (a : ↥N) → T)
          x_1 :
        T)
⊢ Eq (α := LinearMap.{u, u, v, w} (RingHom.id R) (↥M ⊗[R] ↥N) T)
    (mulMap
        (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)
        (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))
    ((↑f : [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T) ∘ₗ
      M.mulMap N)

Tactic:
ext