awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
single :
  Eq (α := M ⊗[R] N) ((Finsupp.single (i', k') (m ⊗ₜ[R] n) : (a : ι × κ) → M ⊗[R] N) (i, k) : M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (Finsupp.single k' n : (a : κ) → N) k : M ⊗[R] N)
single₁ :
  Eq (α := M ⊗[R] N) (if (i', k') = (i, k) then m ⊗ₜ[R] n else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
single₂ :
  Eq (α := M ⊗[R] N) (if i' = i ∧ k' = k then m ⊗ₜ[R] n else 0)
    ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (Finsupp.single k' n : (a : κ) → N) k : M ⊗[R] N)
have single₃ : Eq (α := M ⊗[R] N) (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0)
  ((if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0)
Tactic: classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
have single : Eq (α := M ⊗[R] N)
  (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
              (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
            (Finsupp.single i' m ⊗ₜ[R] 0) :
          ι × κ →₀ M ⊗[R] N) :
        (a : ι × κ) → M ⊗[R] N)
      (i, k) :
    M ⊗[R] N)
  ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (0 : (a : κ) → N) k : M ⊗[R] N)
Tactic: induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
single :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] 0) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (0 : (a : κ) → N) k : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
have single₁ : ∀ (g₁ g₂ : κ →₀ N)
  (hg₁ :
    Eq (α := M ⊗[R] N)
      (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                  (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                (Finsupp.single i' m ⊗ₜ[R] g₁) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₁ : (a : κ) → N) k : M ⊗[R] N))
  (hg₂ :
    Eq (α := M ⊗[R] N)
      (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                  (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                (Finsupp.single i' m ⊗ₜ[R] g₂) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₂ : (a : κ) → N) k : M ⊗[R] N)),
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (Finsupp.single i' m ⊗ₜ[R] (g₁ + g₂)) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((Finsupp.single i' m : (a : ι) → M) i ⊗ₜ[R] (g₁ + g₂ : (a : κ) → N) k : M ⊗[R] N)
Tactic: induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (f ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
have zero : Eq (α := M ⊗[R] N)
  (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
              (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
            (0 ⊗ₜ[R] g) :
          ι × κ →₀ M ⊗[R] N) :
        (a : ι × κ) → M ⊗[R] N)
      (i, k) :
    M ⊗[R] N)
  ((0 : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
Tactic: induction f using Finsupp.induction_linear with
  | zero => simp
  | add f₁ f₂ hf₁ hf₂ => simp [add_tmul, hf₁, hf₂]
  | single i' m =>
    induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Semiring S
inst_6 : Algebra R S
inst_7 : Module S M
inst_8 : IsScalarTower R S M
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
zero :
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (0 ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((0 : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              (f ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
have add : ∀ (f₁ f₂ : ι →₀ M)
  (hf₁ :
    Eq (α := M ⊗[R] N)
      (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                  (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                (f₁ ⊗ₜ[R] g) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((f₁ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N))
  (hf₂ :
    Eq (α := M ⊗[R] N)
      (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                  (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
                (f₂ ⊗ₜ[R] g) :
              ι × κ →₀ M ⊗[R] N) :
            (a : ι × κ) → M ⊗[R] N)
          (i, k) :
        M ⊗[R] N)
      ((f₂ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)),
  Eq (α := M ⊗[R] N)
    (((((finsuppTensorFinsupp R S M N ι κ : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N) :
                (a : (ι →₀ M) ⊗[R] (κ →₀ N)) → ι × κ →₀ M ⊗[R] N)
              ((f₁ + f₂) ⊗ₜ[R] g) :
            ι × κ →₀ M ⊗[R] N) :
          (a : ι × κ) → M ⊗[R] N)
        (i, k) :
      M ⊗[R] N)
    ((f₁ + f₂ : (a : ι) → M) i ⊗ₜ[R] (g : (a : κ) → N) k : M ⊗[R] N)
Tactic: induction f using Finsupp.induction_linear with
  | zero => simp
  | add f₁ f₂ hf₁ hf₂ => simp [add_tmul, hf₁, hf₂]
  | single i' m =>
    induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
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) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ R) ⊗[R] (κ →₀ R))
have nth_rw : Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R))
  ((LinearEquiv.symm (finsuppTensorFinsupp' R ι κ) : (a : ι × κ →₀ R) → (ι →₀ R) ⊗[R] (κ →₀ R))
      (Finsupp.single i (1 * r)) :
    (ι →₀ R) ⊗[R] (κ →₀ R))
  (Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r : (ι →₀ R) ⊗[R] (κ →₀ R))
Tactic: nth_rw 1 [← one_mul r]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
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) :
      (ι →₀ R) ⊗[R] (κ →₀ R))
    (Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1 : (ι →₀ R) ⊗[R] (κ →₀ R))
have 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))
Tactic: nth_rw 1 [← mul_one r]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
ι : Type u_5
κ : Type u_6
inst : CommSemiring R
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsupp' R ι κ)
have rw : Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsuppLid R R ι κ)
Tactic: rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
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 ι κ)
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsupp' R ι κ)
have 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)
Tactic: rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
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)
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsupp' R ι κ)
have 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)
Tactic: rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
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)
⊢ Eq (α := (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R) (finsuppTensorFinsuppRid R R ι κ) (finsuppTensorFinsupp' R ι κ)
have 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)
Tactic: rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]
-- 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₁
ι₂ : 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)
have toFun : ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
Tactic: refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right
-- 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₁
ι₂ : 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₁'
toFun :
  ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
have invFun : (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
Tactic: refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right
-- 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₁
ι₂ : 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₁'
toFun :
  ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
invFun :
  (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S] (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂
⊢ ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) ≃ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)
have left : Eq (α :=
  (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S]
    ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
  ((AlgebraTensorModule.lift
        (toModule S ι₁ (M := M₁)
          ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) fun (i₁ : ι₁) ↦
          LinearMap.flip
            (toModule R ι₂ (M := M₂) (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
              fun (i₂ : ι₂) ↦
              LinearMap.flip
                (AlgebraTensorModule.curry
                    (lof S (ι₁ × ι₂) (fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) (i₁, i₂)) :
                  M₁ i₁ →ₗ[S] M₂ i₂ →ₗ[R] ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)))) :
      ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) →ₗ[S]
        ⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) ∘ₗ
    (toModule S (ι₁ × ι₂) (M := fun (i : ι₁ × ι₂) ↦ TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2))
        ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun (i : ι₁ × ι₂) ↦
        AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2) :
      (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) →ₗ[S]
        (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂))
  LinearMap.id
Tactic: refine LinearEquiv.ofLinear ?toFun ?invFun ?left ?right
-- 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₁
ι₂ : 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₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
    (((LinearEquiv.symm (TensorProduct.directSum R S M₁ M₂) :
            (⨁ (i : ι₁ × ι₂), TensorProduct.{u, w₁, w₂} R (M₁ i.1) (M₂ i.2)) ≃ₗ[S]
              (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) :
          (a : ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) → (⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
        (((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₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂)
    ((lof S ι₁ M₁ i₁ : (a : M₁ i₁) → ⨁ (i : ι₁), M₁ i) m₁ ⊗ₜ[R] (lof R ι₂ M₂ i₂ : (a : M₂ i₂) → ⨁ (i : ι₂), M₂ i) m₂ :
      (⨁ (i : ι₁), M₁ i) ⊗[R] ⨁ (i : ι₂), M₂ i)
have rw : Eq (α := ⨁ (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))
  (((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))
Tactic: rw [LinearEquiv.symm_apply_eq, directSum_lof_tmul_lof]