-- Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct
Goal:
R : Type u
inst : CommSemiring R
ι₁ : Type v₁
inst_1 : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst_2 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_3 : AddCommMonoid M₁'
inst_4 : AddCommMonoid M₂'
inst_5 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_6 : Module R M₁'
inst_7 : Module R M₂'
f : M₁' →ₗ[R] M₂'
a :
  ∀ (x : M₁') (i : ι₁) (x_1 : M₁ i) (i_1 : ι₁),
    (((((AlgebraTensorModule.curry
                          (((↑(directSumRight R R M₂' M₁) :
                                (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
                              (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
                            (rTensor (⨁ (i : ι₁), M₁ i) f :
                              (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] M₂' ⊗[R] ⨁ (i : ι₁), M₁ i)) :
                        M₁' →ₗ[R] (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
                      (a : M₁') → (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
                    x ∘ₗ
                  lof R ι₁ M₁ i :
                (a : M₁ i) → ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
              x_1 :
            ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
          (a : ι₁) → M₂' ⊗[R] M₁ a)
        i_1 =
      (((((AlgebraTensorModule.curry
                          ((lmap (M := fun (x : ι₁) ↦ TensorProduct.{u, w₁', w₁} R M₁' (M₁ x)) (N := fun (x : ι₁) ↦
                                TensorProduct.{u, w₂', w₁} R M₂' (M₁ x)) fun (x : ι₁) ↦ rTensor (M₁ x) f :
                              (⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) →ₗ[R]
                                ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
                            ((↑(directSumRight R R M₁' M₁) :
                                (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) :
                              (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i))) :
                        M₁' →ₗ[R] (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
                      (a : M₁') → (⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
                    x ∘ₗ
                  lof R ι₁ M₁ i :
                (a : M₁ i) → ⨁ (i : ι₁), M₂' ⊗[R] M₁ i)
              x_1 :
            ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
          (a : ι₁) → M₂' ⊗[R] M₁ a)
        i_1
⊢ Eq (α := (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i))
    (((↑(directSumRight R R M₂' M₁) :
            (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) :
          (M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
        (rTensor (⨁ (i : ι₁), M₁ i) f : (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] M₂' ⊗[R] ⨁ (i : ι₁), M₁ i) :
      (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i))
    ((lmap (M := fun (x : ι₁) ↦ TensorProduct.{u, w₁', w₁} R M₁' (M₁ x)) (N := fun (x : ι₁) ↦
            TensorProduct.{u, w₂', w₁} R M₂' (M₁ x)) fun (x : ι₁) ↦ rTensor (M₁ x) f :
          (⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) →ₗ[R]
            ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i)) ∘ₗ
        ((↑(directSumRight R R M₁' M₁) :
            (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) :
          (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₁', w₁} R M₁' (M₁ i)) :
      (M₁' ⊗[R] ⨁ (i : ι₁), M₁ i) →ₗ[R] ⨁ (i : ι₁), TensorProduct.{u, w₂', w₁} R M₂' (M₁ i))

Tactic:
ext