-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.TensorProduct (goal)
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_1 : ⨁ (i : ι₂), M₂ i
i j : ι₂
n : M₂ j
pos :
  ∀ (hj : j = i),
    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 (α := 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))
have neg : ∀ (hj : ¬j = i),
  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))
Tactic: by_cases hj : j = i