awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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₂')

Tactic:
simp [DirectSum.component.of, hj]

Premises used: DirectSum.component.of
-- 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₁'
x : M₁'
i : ι₂
y : M₂ i
⊢ (PUnit.unit, i) = ((Equiv.uniqueProd ι₂ Unit).symm : (a : ι₂) → Unit × ι₂) i

Tactic:
simp
-- 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₁'
x : M₁'
i : ι₂
y : M₂ i
⊢ Eq (α := ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((directSumRight R S M₁' M₂ :
            (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
            TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))

Tactic:
simpa [directSumRight] using lequivCongrLeft_lof S (by simp) _ _ rfl

Premises used: TensorProduct.directSumRight, DirectSum.lequivCongrLeft_lof, rfl
-- 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₁'
x : M₁'
i : ι₂
y : M₂ i
rw :
  Eq (α := ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
            TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((directSumRight R S M₁' M₂ :
            (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
rw₁ rw₂ :
  Eq (α := ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
            TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
    (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
            TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
          (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i))
⊢ Eq (α := M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
    (((LinearEquiv.symm (directSumRight R S M₁' M₂) :
            (⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) ≃ₗ[S] M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) :
          (a : ⨁ (i : ι₂), M₁' ⊗[R] M₂ i) → M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
        (((lof S ι₂ (fun (i : ι₂) ↦ TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) i :
              TensorProduct.{u, w₁', w₂} R M₁' (M₂ i) →ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
            (a : M₁' ⊗[R] M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
          (x ⊗ₜ[R] y)) :
      M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)
    (x ⊗ₜ[R] (lof R ι₂ M₂ i : (a : M₂ i) → ⨁ (i : ι₂), M₂ i) y : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i)

Tactic:
rw [LinearEquiv.symm_apply_eq, directSumRight_tmul_lof]

Premises used: LinearEquiv.symm_apply_eq, TensorProduct.directSumRight_tmul_lof
-- 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₂'
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

Tactic:
simp
-- 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 : ι₂
this :
  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)
⊢ ((((directSumRight R S M₁' M₂ :
                (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
              (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            (m ⊗ₜ[R] n) :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i =
    m ⊗ₜ[R] (n : (a : ι₂) → M₂ a) i

Tactic:
simpa using LinearMap.congr_fun this n

Premises used: LinearMap.congr_fun
-- 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 : ι₂
suffices :
  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)
⊢ ((((directSumRight R S M₁' M₂ :
                (M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) ≃ₗ[S] ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
              (a : M₁' ⊗[R] ⨁ (i : ι₂), M₂ i) → ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
            (m ⊗ₜ[R] n) :
          ⨁ (i : ι₂), TensorProduct.{u, w₁', w₂} R M₁' (M₂ i)) :
        (a : ι₂) → M₁' ⊗[R] M₂ a)
      i =
    m ⊗ₜ[R] (n : (a : ι₂) → M₂ a) i

Tactic:
suffices (DirectSum.component S ι₂ _ i).restrictScalars R ∘ₗ
      (directSumRight R S M₁' M₂).toLinearMap.restrictScalars R ∘ₗ
        (TensorProduct.mk R M₁' (⨁ i, M₂ i) m) =
          (TensorProduct.mk R M₁' (M₂ i) m) ∘ₗ (DirectSum.component R ι₂ M₂ i) by
    simpa using LinearMap.congr_fun this n
-- 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_1 : ⨁ (i : ι₂), M₂ i
j : ι₂
n : M₂ j
⊢ Eq (α := TensorProduct.{u, w₁', w₂} R M₁' (M₂ j))
    ((((↑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)) j) ∘ₗ
              (↑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₂ j)
        n :
      TensorProduct.{u, w₁', w₂} R M₁' (M₂ j))
    ((((mk R M₁' (M₂ j) : (a : M₁') → M₂ j →ₗ[R] M₁' ⊗[R] M₂ j) m ∘ₗ component R ι₂ M₂ j) ∘ₗ lof R ι₂ M₂ j :
          (a : M₂ j) → M₁' ⊗[R] M₂ j)
        n :
      TensorProduct.{u, w₁', w₂} R M₁' (M₂ j))

Tactic:
simp
-- 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_1 : ⨁ (i : ι₂), M₂ i
i j : ι₂
n : M₂ j
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:
simp [DirectSum.component.of, hj]

Premises used: DirectSum.component.of
-- Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct
Goal:
R : Type u
inst : CommSemiring R
S : Type u_2
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₁'
S₀ : Type u_1
inst_10 : CommSemiring S₀
inst_11 : Algebra R S₀
inst_12 : Algebra S₀ S
inst_13 : Module S₀ M₁'
inst_14 : IsScalarTower R S₀ M₁'
inst_15 : IsScalarTower S₀ S M₁'
a :
  ∀ (x : M₁') (i : ι₂) (x_1 : M₂ i) (i_1 : ι₂),
    (((((AlgebraTensorModule.curry
                          (↑(LinearEquiv.restrictScalars R
                                (LinearEquiv.restrictScalars S₀
                                  (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) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] 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
                          (↑(LinearEquiv.restrictScalars R
                                (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) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] 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))
    (↑(LinearEquiv.restrictScalars R
          (LinearEquiv.restrictScalars S₀
            (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) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)
    (↑(LinearEquiv.restrictScalars R
          (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) →ₗ[R] ⨁ (i : ι₂), M₁' ⊗[R] M₂ i)

Tactic:
ext