-- Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct
Goal:
R : Type u
inst : CommSemiring R
S : Type u_1
inst_1 : Semiring S
inst_2 : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst_3 : DecidableEq ι₁
inst_4 : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_6 : AddCommMonoid M₁'
inst_7 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_8 : AddCommMonoid M₂'
inst_9 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_10 : Module R M₁'
inst_11 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_12 : Module R M₂'
inst_13 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_14 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
inst_15 : Module S M₁'
inst_16 : IsScalarTower R S M₁'
i₁ : ι₁
i₂ : M₁ i₁
x₁ : ι₂
x₂ : M₂ x₁
⊢ Eq (α := (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
    ((((AlgebraTensorModule.curry
                      ((toModule S (ι₁ × ι₂) (M := fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
                          ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun (i : ι₁ × ι₂) ↦
                          AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
                        AlgebraTensorModule.lift
                          (toModule S ι₁ (M := M₁)
                            ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
                            fun (i₁ : ι₁) ↦
                            LinearMap.flip
                              (toModule R ι₂ (M := M₂)
                                (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
                                fun (i₂ : ι₂) ↦
                                LinearMap.flip
                                  (AlgebraTensorModule.curry
                                      (lof S (ι₁ × ι₂)
                                        (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) :
                                    M₁ i₁ →ₗ[S]
                                      M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))))) ∘ₗ
                    lof S ι₁ M₁ i₁ :
                  M₁ i₁ →ₗ[S] (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) :
                (a : M₁ i₁) → (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
              i₂ ∘ₗ
            lof R ι₂ M₂ x₁ :
          (a : M₂ x₁) → (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
        x₂ :
      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
    ((((AlgebraTensorModule.curry LinearMap.id ∘ₗ lof S ι₁ M₁ i₁ :
                  M₁ i₁ →ₗ[S] (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) :
                (a : M₁ i₁) → (⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
              i₂ ∘ₗ
            lof R ι₂ M₂ x₁ :
          (a : M₂ x₁) → (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
        x₂ :
      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)

Tactic:
simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
      coe_restrictScalars, AlgebraTensorModule.lift_apply, lift.tmul, toModule_lof, flip_apply,
      AlgebraTensorModule.map_tmul, id_coe, id_eq]

Premises used: LinearMap.id_coe, LinearMap.coe_restrictScalars, TensorProduct.lift.tmul, LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.coe_comp, DirectSum.toModule_lof, TensorProduct.AlgebraTensorModule.lift_apply, TensorProduct.curry_apply, TensorProduct.AlgebraTensorModule.map_tmul, Function.comp_apply, id_eq