-- 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
x : ↥M
x_1 : ↥N
a :
  HMul.hMul (α := T)
      (↑((LinearMap.submoduleMap
                (↑f :
                  [inst_5 : FunLike (S →ₐ[R] T) S T] → [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                M :
              (a : ↥M) →
                ↥(map
                    (↑f :
                      [inst_5 : FunLike (S →ₐ[R] T) S T] →
                        [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                    M))
            x) :
        T)
      (↑((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 : ↥N) →
                ↥(map
                    (↑f :
                      [inst_5 : FunLike (S →ₐ[R] T) S T] →
                        [SemilinearMapClass (S →ₐ[R] T) (RingHom.id R) S T] → S →ₗ[R] T)
                    N))
            x_1) :
        T) =
    HMul.hMul (α := T) (β := T) ((f : (a : S) → T) (↑x : S) : T) ((f : (a : S) → T) (↑x_1 : S) : T)
⊢ 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)

Tactic:
simp only [TensorProduct.AlgebraTensorModule.curry_apply,
    TensorProduct.curry_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
    Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul, LinearMap.coe_coe, map_mul]

Premises used: Submodule.mulMap_tmul, LinearMap.coe_restrictScalars, TensorProduct.AlgebraTensorModule.curry_apply, map_mul, LinearMap.coe_comp, TensorProduct.curry_apply, TensorProduct.map_tmul, Function.comp_apply, LinearMap.coe_coe