-- 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₂
inst_3 : DecidableEq ι₂
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
inst_4 : AddCommMonoid M₁'
inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_6 : Module R M₁'
inst_7 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_8 : Module S M₁'
inst_9 : IsScalarTower R S M₁'
m : M₁'
n : ⨁ (i : ι₂), M₂ i
i : ι₂
H :
  ∀ (j : ι₂) (n : M₂ j),
    Eq (α := TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
      ((((↑R :
                    {S : Type u_1} →
                      {M : Type (max v₂ w₁' w₂)} →
                        {M₂ : Type (max w₁' w₂)} →
                          [inst : Semiring R] →
                            [inst_10 : Semiring S] →
                              [inst_11 : AddCommMonoid M] →
                                [inst_12 : AddCommMonoid M₂] →
                                  [inst_13 : Module R M] →
                                    [inst_14 : Module R M₂] →
                                      [inst_15 : Module S M] →
                                        [inst_16 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                  (component S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i) ∘ₗ
                (↑R :
                      {S : Type u_1} →
                        {M M₂ : Type (max (max v₂ w₁') w₂)} →
                          [inst : Semiring R] →
                            [inst_10 : Semiring S] →
                              [inst_11 : AddCommMonoid M] →
                                [inst_12 : AddCommMonoid M₂] →
                                  [inst_13 : Module R M] →
                                    [inst_14 : Module R M₂] →
                                      [inst_15 : Module S M] →
                                        [inst_16 : Module S M₂] →
                                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                    ((↑(directSumRight R S M₁' M₂) :
                        (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
                      (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) ∘ₗ
                  (mk R M₁' (⨁ (i : ι₂), M₂ i) : (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) m) ∘ₗ
              lof R ι₂ M₂ j :
            (a : M₂ j) → M₁' ⊗[R] M₂ i)
          n :
        TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
      ((((mk R M₁' (M₂ i) : (a : M₁') → M₂ i →ₗ[R] M₁' ⊗[R] M₂ i) m ∘ₗ component R ι₂ M₂ i) ∘ₗ lof R ι₂ M₂ j :
            (a : M₂ j) → M₁' ⊗[R] M₂ i)
          n :
        TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
⊢ Eq (α := (⨁ (i : ι₂), M₂ i) →ₗ[R] TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    ((↑R :
          {S : Type u_1} →
            {M : Type (max v₂ w₁' w₂)} →
              {M₂ : Type (max w₁' w₂)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (component S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i) ∘ₗ
      (↑R :
            {S : Type u_1} →
              {M M₂ : Type (max (max v₂ w₁') w₂)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          ((↑(directSumRight R S M₁' M₂) :
              (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
            (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) ∘ₗ
        (mk R M₁' (⨁ (i : ι₂), M₂ i) : (a : M₁') → (⨁ (i : ι₂), M₂ i) →ₗ[R] M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) m)
    ((mk R M₁' (M₂ i) : (a : M₁') → M₂ i →ₗ[R] M₁' ⊗[R] M₂ i) m ∘ₗ component R ι₂ M₂ i)

Tactic:
ext j n