-- 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₂ : ι₂
x₁ : M₁ (i₁, i₂).1
x₂ : M₂ (i₁, i₂).2
⊢ Eq (α := ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    (((((AlgebraTensorModule.curry
                    (((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)))) :
                          ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S]
                            ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) ∘ₗ
                        (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) :
                          (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S]
                            (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)) ∘ₗ
                      lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) :
                  M₁ (i₁, i₂).1 →ₗ[S]
                    M₂ (i₁, i₂).2 →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
                (a : M₁ (i₁, i₂).1) → M₂ (i₁, i₂).2 →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
              x₁ :
            M₂ (i₁, i₂).2 →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
          (a : M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
        x₂ :
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    (((((AlgebraTensorModule.curry
                    (LinearMap.id ∘ₗ
                      lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) :
                  M₁ (i₁, i₂).1 →ₗ[S]
                    M₂ (i₁, i₂).2 →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
                (a : M₁ (i₁, i₂).1) → M₂ (i₁, i₂).2 →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
              x₁ :
            M₂ (i₁, i₂).2 →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
          (a : M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
        x₂ :
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))

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

Premises used: 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, LinearMap.id_comp