awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r : R
nth_rw :
  Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (r * 1)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1 : (ι →₀ R) ⊗[R] (κ →₀ R))
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R)) (Finsupp.single i r) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1 : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
nth_rw 1 [← mul_one r]

Premises used: mul_one
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r : R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (r * 1)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1 : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Premises used: finsuppTensorFinsupp'_symm_single_mul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
i : ι × κ
r : R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
    ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
        (Finsupp.single i (r * 1)) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1 : (ι →₀ R) ⊗[R] (κ →₀ R))

Tactic:
exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Premises used: finsuppTensorFinsupp'_symm_single_mul
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppLid R R ι κ) (finsuppTensorFinsupp' R ι κ)

Tactic:
rfl

Premises used: finsuppTensorFinsupp', rfl
-- Module: Mathlib.LinearAlgebra.DirectSum.Finsupp
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
rw :
  Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsuppLid R R ι κ)
rw₁ :
  finsuppTensorFinsuppRid R R ι κ =
    LinearEquiv.trans (module_M₂ := Finsupp.module (ι × κ) (R ⊗[R] R))
      (finsuppTensorFinsupp R R R R ι κ : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R ⊗[R] R)
      (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R R) : (ι × κ →₀ R ⊗[R] R) ≃ₗ[R] ι × κ →₀ R)
rw₂ :
  Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R)
    (LinearEquiv.trans (module_M₂ := Finsupp.module (ι × κ) (R ⊗[R] R))
        (finsuppTensorFinsupp R R R R ι κ : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R ⊗[R] R)
        (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R) : (ι × κ →₀ R ⊗[R] R) ≃ₗ[R] ι × κ →₀ R) :
      (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R)
    (LinearEquiv.trans (module_M₂ := Finsupp.module (ι × κ) (R ⊗[R] R))
        (finsuppTensorFinsupp R R R R ι κ : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R ⊗[R] R)
        (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R R) : (ι × κ →₀ R ⊗[R] R) ≃ₗ[R] ι × κ →₀ R) :
      (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R)
rw₃ rw₄ :
  Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R)
    (LinearEquiv.trans (module_M₂ := Finsupp.module (ι × κ) (R ⊗[R] R))
        (finsuppTensorFinsupp R R R R ι κ : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R ⊗[R] R)
        (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R) : (ι × κ →₀ R ⊗[R] R) ≃ₗ[R] ι × κ →₀ R) :
      (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R)
    (LinearEquiv.trans (module_M₂ := Finsupp.module (ι × κ) (R ⊗[R] R))
        (finsuppTensorFinsupp R R R R ι κ : (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R ⊗[R] R)
        (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R R) : (ι × κ →₀ R ⊗[R] R) ≃ₗ[R] ι × κ →₀ R) :
      (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R)
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsupp' R ι κ)

Tactic:
rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]

Premises used: finsuppTensorFinsuppLid, TensorProduct.lid_eq_rid, finsuppTensorFinsuppRid, finsuppTensorFinsupp'
-- 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₁
ι₂ : Type v₂
inst_3 : DecidableEq ι₁
inst_4 : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_6 : AddCommMonoid M₁'
inst_7 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_8 : AddCommMonoid M₂'
inst_9 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_10 : Module R M₁'
inst_11 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_12 : Module R M₂'
inst_13 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_14 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
inst_15 : Module S M₁'
inst_16 : IsScalarTower R S M₁'
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)

Tactic:
exact AlgebraTensorModule.lift <|
      toModule S _ _ fun i₁ => flip <| toModule R _ _ fun i₂ => flip <| AlgebraTensorModule.curry <|
      DirectSum.lof S (ι₁ × ι₂) (fun i => M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂)

Premises used: Prod.mk, LinearMap, Prod.fst, DirectSum.toModule, LinearMap.flip, DirectSum.lof, TensorProduct, Prod, RingHom.id, TensorProduct.AlgebraTensorModule.curry, Prod.snd, DirectSum, TensorProduct.AlgebraTensorModule.lift
-- 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₁
ι₂ : Type v₂
inst_3 : DecidableEq ι₁
inst_4 : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_6 : AddCommMonoid M₁'
inst_7 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_8 : AddCommMonoid M₂'
inst_9 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_10 : Module R M₁'
inst_11 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_12 : Module R M₂'
inst_13 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_14 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
inst_15 : Module S M₁'
inst_16 : IsScalarTower R S M₁'
⊢ (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂

Tactic:
exact toModule S _ _ fun i => AlgebraTensorModule.map (lof S _ M₁ i.1) (lof R _ M₂ i.2)

Premises used: DirectSum.toModule, TensorProduct.AlgebraTensorModule.map
-- 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₁
ι₂ : Type v₂
inst_3 : DecidableEq ι₁
inst_4 : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₂ : ι₂ → Type w₂
inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst_7 : (i₁ : ι₁) → Module.{u, w₁} R (M₁ i₁)
inst_8 : (i₂ : ι₂) → Module.{u, w₂} R (M₂ i₂)
inst_9 : (i₁ : ι₁) → Module.{u_1, w₁} S (M₁ i₁)
inst_10 : ∀ (i₁ : ι₁), IsScalarTower.{u, u_1, w₁} R S (M₁ i₁)
i₁ : ι₁
m₁ : M₁ i₁
i₂ : ι₂
m₂ : M₂ i₂
⊢ Eq (α := ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    (((TensorProduct.directSum R S M₁ M₂ :
            ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[S]
              ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
          (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
        ((lof S ι₁ M₁ i₁ : (a : M₁ i₁) → ⨁ (i : ι₁), M₁ i) m₁ ⊗ₜ[R]
          (lof R ι₂ M₂ i₂ : (a : M₂ i₂) → ⨁ (i : ι₂), M₂ i) m₂) :
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
    (((lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂) :
            TensorProduct.{u, w₁, w₂} R (M₁ (i₁, i₂).1) (M₂ (i₁, i₂).2) →ₗ[S]
              ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) :
          (a : M₁ (i₁, i₂).1 ⊗[R] M₂ (i₁, i₂).2) → ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2)
        (m₁ ⊗ₜ[R] m₂) :
      ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))

Tactic:
simp [TensorProduct.directSum]

Premises used: TensorProduct.directSum
-- 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₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ (i, PUnit.unit) = ((Equiv.prodUnique ι₁ 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 : (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₁)
i : ι₁
x : M₁ i
y : M₂'
⊢ Eq (α := ⨁ (i : ι₁), 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₂') :
          (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
        ((lof S ι₁ M₁ i : (a : M₁ i) → ⨁ (i : ι₁), M₁ i) x ⊗ₜ[R] y) :
      ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')
    (((lof S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') i :
            TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂' →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
          (a : M₁ i ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
        (x ⊗ₜ[R] y) :
      ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂')

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

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

Tactic:
rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]

Premises used: LinearEquiv.symm_apply_eq, TensorProduct.directSumLeft_tmul_lof
-- 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 : M₂'
i : ι₁
this :
  Eq (α := (⨁ (i : ι₁), M₁ i) →ₗ[S] 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 :
              (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
          (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
      (⨁ (i : ι₁), M₁ i) →ₗ[S] 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 ∘ₗ
        component S ι₁ M₁ i :
      (⨁ (i : ι₁), M₁ i) →ₗ[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₂') :
              (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
            (m ⊗ₜ[R] n) :
          ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : ι₁) → M₁ a ⊗[R] M₂')
      i =
    (m : (a : ι₁) → M₁ a) i ⊗ₜ[R] n

Tactic:
simpa using LinearMap.congr_fun this m

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 : (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 : M₂'
i : ι₁
suffices :
  Eq (α := (⨁ (i : ι₁), M₁ i) →ₗ[S] 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 :
              (⨁ (i : ι₁), M₁ i) →ₗ[S] (⨁ (i : ι₁), M₁ i) ⊗[R] M₂') :
          (⨁ (i : ι₁), M₁ i) →ₗ[S] ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
      (⨁ (i : ι₁), M₁ i) →ₗ[S] 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 ∘ₗ
        component S ι₁ M₁ i :
      (⨁ (i : ι₁), M₁ i) →ₗ[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₂') :
              (a : (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] M₂') → ⨁ (i : ι₁), M₁ i ⊗[R] M₂')
            (m ⊗ₜ[R] n) :
          ⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') :
        (a : ι₁) → M₁ a ⊗[R] M₂')
      i =
    (m : (a : ι₁) → M₁ a) i ⊗ₜ[R] n

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

Tactic:
ext j 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 : (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₂'
j : ι₁
n : M₁ j
⊢ Eq (α := TensorProduct.{u, w₁, w₂'} R (M₁ j) M₂')
    (((((component S ι₁ (fun (i : ι₁) ↦ TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') j :
                  (⨁ (i : ι₁), TensorProduct.{u, w₁, w₂'} R (M₁ i) M₂') →ₗ[S]
                    TensorProduct.{u, w₁, w₂'} R (M₁ j) 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₁ j) M₂') :
          (a : M₁ j) → M₁ j ⊗[R] M₂')
        n :
      TensorProduct.{u, w₁, w₂'} R (M₁ j) M₂')
    ((((LinearMap.flip (AlgebraTensorModule.mk R S (M₁ j) M₂') : (a : M₂') → M₁ j →ₗ[S] M₁ j ⊗[R] M₂') n_1 ∘ₗ
              component S ι₁ M₁ j) ∘ₗ
            lof S ι₁ M₁ j :
          (a : M₁ j) → M₁ j ⊗[R] M₂')
        n :
      TensorProduct.{u, w₁, w₂'} R (M₁ j) M₂')

Tactic:
simp