-- 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₁'
left :
  ∀ (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))
⊢ Eq (α :=
    (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S]
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (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)))) :
        ((⨁ (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₂))
    LinearMap.id

Tactic:
ext ⟨i₁, i₂⟩ x₁ x₂ : 4