-- 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 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_5 : AddCommMonoid M₂'
inst_6 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_7 : Module R M₂'
inst_8 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_9 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n_1 : M₂'
i j : ι₁
n : M₁ j
pos :
  ∀ (hj : j = i),
    Eq (α := TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
      (((((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
                    (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S]
                      TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                  (((↑(directSumLeft R S M₁ M₂') :
                          (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
                        (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                      ((LinearMap.flip (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂') :
                            (a : M₂') → (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
                          n_1 :
                        (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
                    (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')) ∘ₗ
                lof S ι₁ M₁ j :
              M₁ j →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
            (a : M₁ j) → M₁ i ⊗[R] M₂')
          n :
        TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
      ((((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ i) M₂') : (a : M₂') → M₁ i →ₗ[S] M₁ i ⊗[R] M₂') n_1 ∘ₗ
                component S ι₁ M₁ i) ∘ₗ
              lof S ι₁ M₁ j :
            (a : M₁ j) → M₁ i ⊗[R] M₂')
          n :
        TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
neg :
  ∀ (hj : ¬j = i),
    Eq (α := TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
      (((((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
                    (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S]
                      TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                  (((↑(directSumLeft R S M₁ M₂') :
                          (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
                        (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                      ((LinearMap.flip (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂') :
                            (a : M₂') → (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
                          n_1 :
                        (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
                    (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')) ∘ₗ
                lof S ι₁ M₁ j :
              M₁ j →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
            (a : M₁ j) → M₁ i ⊗[R] M₂')
          n :
        TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
      ((((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ i) M₂') : (a : M₂') → M₁ i →ₗ[S] M₁ i ⊗[R] M₂') n_1 ∘ₗ
                component S ι₁ M₁ i) ∘ₗ
              lof S ι₁ M₁ j :
            (a : M₁ j) → M₁ i ⊗[R] M₂')
          n :
        TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
⊢ Eq (α := TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    (((((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
                  (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S]
                    TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                (((↑(directSumLeft R S M₁ M₂') :
                        (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
                      (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') ∘ₗ
                    ((LinearMap.flip (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂') :
                          (a : M₂') → (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂')
                        n_1 :
                      (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
                  (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')) ∘ₗ
              lof S ι₁ M₁ j :
            M₁ j →ₗ[S] TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
          (a : M₁ j) → M₁ i ⊗[R] M₂')
        n :
      TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    ((((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ i) M₂') : (a : M₂') → M₁ i →ₗ[S] M₁ i ⊗[R] M₂') n_1 ∘ₗ
              component S ι₁ M₁ i) ∘ₗ
            lof S ι₁ M₁ j :
          (a : M₁ j) → M₁ i ⊗[R] M₂')
        n :
      TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')

Tactic:
by_cases hj : j = i