-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Submodule (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
T : Type w
inst_3 : Semiring T
inst_4 : Algebra R T
f : S →ₐ[R] T
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)
have 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)
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]