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
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
t : M ⊗[R] (ι →₀ N)
i : ι
zero :
  Eq (α := M ⊗[R] N)
    ((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) 0 :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) 0 : M ⊗[R] N)
tmul :
  ∀ (m : M) (f : ι →₀ N),
    Eq (α := M ⊗[R] N)
      (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
                (m ⊗ₜ[R] f) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) (m ⊗ₜ[R] f) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) t :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) t : M ⊗[R] N)
have add : ∀ (x y : M ⊗[R] (ι →₀ N))
  (hx :
    Eq (α := M ⊗[R] N)
      (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) x :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) x : M ⊗[R] N))
  (hy :
    Eq (α := M ⊗[R] N)
      (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N) y :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) y : M ⊗[R] N)),
  Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
              (x + y) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((lTensor M (Finsupp.lapply i) : (a : M ⊗[R] (ι →₀ N)) → M ⊗[R] N) (x + y) : M ⊗[R] N)
Tactic: induction t with
  | zero => simp
  | tmul m f => simp [finsuppRight_apply_tmul_apply]
  | add x y hx hy => simp [map_add, hx, hy]
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
i : ι
m : M
n : N
⊢ Eq (α := ι →₀ M ⊗[R] N)
    (((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
        (m ⊗ₜ[R] Finsupp.single i n) :
      ι →₀ M ⊗[R] N)
    (Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have h : ∀ (a : ι),
  Eq (α := M ⊗[R] N)
    (((((finsuppRight R S M N ι : M ⊗[R] (ι →₀ N) ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : M ⊗[R] (ι →₀ N)) → ι →₀ M ⊗[R] N)
              (m ⊗ₜ[R] Finsupp.single i n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        a :
      M ⊗[R] N)
    ((Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) a : M ⊗[R] N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
⊢ Eq (α := ι →₀ N) ((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N)
    (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : ι →₀ N)
have h : ∀ (i : ι),
  Eq.{u_4 + 1} (α := N)
    ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
    ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
⊢ Eq.{u_4 + 1} (α := N)
    ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
    ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)
have h : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
  (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i
Tactic: rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
h :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i
⊢ Eq.{u_4 + 1} (α := N)
    ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
    ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)
have h₁ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
  p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • n) : (a : ι) → N) i
Tactic: rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
h :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i
h₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • n) : (a : ι) → N) i
⊢ Eq.{u_4 + 1} (α := N)
    ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
    ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)
have h₂ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
  (Finsupp.single i (HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n) : (a : ι) → N) i
Tactic: rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
inst : CommSemiring R
N : Type u_4
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_5
inst_3 : DecidableEq ι
p : ι →₀ R
n : N
i : ι
h :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    (p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i
h₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • n) : (a : ι) → N) i
h₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
    (Finsupp.single i (HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n) : (a : ι) → N) i
⊢ Eq.{u_4 + 1} (α := N)
    ((((finsuppScalarLeft R N ι : (a : (ι →₀ R) ⊗[R] N) → ι →₀ N) (p ⊗ₜ[R] n) : ι →₀ N) : (a : ι) → N) i : N)
    ((p.sum fun (i : ι) (m : R) ↦ Finsupp.single i (m • n) : (a : ι) → N) i : N)
have h₃ : HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n =
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((p : (a : ι) → R) i : R) n
Tactic: rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
⊢ Eq (α := ι →₀ M)
    (((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
      ι →₀ M)
    (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : ι →₀ M)
have h : ∀ (i : ι),
  Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
            ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
⊢ Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
            ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)
have h : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
  (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i
Tactic: rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
h :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i
⊢ Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
            ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)
have h₁ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
  p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • m) : (a : ι) → M) i
Tactic: rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
h :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i
h₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • m) : (a : ι) → M) i
⊢ Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
            ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)
have h₂ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
  (Finsupp.single i (HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m) : (a : ι) → M) i
Tactic: rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
ι : Type u_5
inst_7 : DecidableEq ι
m : M
p : ι →₀ R
i : ι
h :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    (p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i
h₁ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    p.sum fun (a₁ : ι) (b : R) ↦ (Finsupp.single a₁ (b • m) : (a : ι) → M) i
h₂ :
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
    (Finsupp.single i (HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m) : (a : ι) → M) i
⊢ Eq.{u_3 + 1} (α := M)
    (((((finsuppScalarRight R S M ι : M ⊗[R] (ι →₀ R) ≃ₗ[S] ι →₀ M) : (a : M ⊗[R] (ι →₀ R)) → ι →₀ M) (m ⊗ₜ[R] p) :
            ι →₀ M) :
          (a : ι) → M)
        i :
      M)
    ((p.sum fun (i : ι) (n : R) ↦ Finsupp.single i (n • m) : (a : ι) → M) i : M)
have h₃ : HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m =
  HSMul.hSMul.{u_1, u_3, u_3} (α := R) ((p : (a : ι) → R) i : R) m
Tactic: rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DirectSum.Finsupp (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
ι : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
inst_5 : DecidableEq ι
v : ι → M
⊢ Eq (α := (ι →₀ S) →ₗ[R] S ⊗[R] M)
    ((↑R :
        {S : Type u_2} →
          {M : Type (max u_2 u_5)} →
            {M₂ : Type (max u_2 u_3)} →
              [inst : Semiring R] →
                [inst_6 : Semiring S] →
                  [inst_7 : AddCommMonoid M] →
                    [inst_8 : AddCommMonoid M₂] →
                      [inst_9 : Module R M] →
                        [inst_10 : Module R M₂] →
                          [inst_11 : Module S M] →
                            [inst_12 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (linearCombination S fun (x : ι) ↦ 1 ⊗ₜ[R] v x))
    (lTensor S (linearCombination R v) ∘ₗ
      (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R)))
have h : ∀ (a : ι) (x : S),
  Eq (α := S ⊗[R] M)
    (((↑R :
                {S : Type u_2} →
                  {M : Type (max u_2 u_5)} →
                    {M₂ : Type (max u_2 u_3)} →
                      [inst : Semiring R] →
                        [inst_6 : Semiring S] →
                          [inst_7 : AddCommMonoid M] →
                            [inst_8 : AddCommMonoid M₂] →
                              [inst_9 : Module R M] →
                                [inst_10 : Module R M₂] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S M₂] →
                                      [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (linearCombination S fun (x : ι) ↦ 1 ⊗ₜ[R] v x) ∘ₗ
            lsingle a :
          (a : S) → S ⊗[R] M)
        x :
      S ⊗[R] M)
    (((lTensor S (linearCombination R v) ∘ₗ
              (↑(LinearEquiv.symm (finsuppScalarRight R R S ι)) : (ι →₀ S) →ₗ[R] S ⊗[R] (ι →₀ R))) ∘ₗ
            lsingle a :
          (a : S) → S ⊗[R] M)
        x :
      S ⊗[R] M)
Tactic: ext
-- 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
⊢ 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: simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
-- 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
⊢ 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)
have pos : i' = i → k' = k → Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
Tactic: split_ifs
-- 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
pos : i' = i → k' = k → Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
⊢ 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)
have neg : i' = i → ¬k' = k → Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] 0)
Tactic: split_ifs
-- 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
pos : i' = i → k' = k → Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
neg : i' = i → ¬k' = k → Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] 0)
⊢ 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)
have pos₁ : ¬i' = i → k' = k → Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] n)
Tactic: split_ifs
-- 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
pos : i' = i → k' = k → Eq (α := M ⊗[R] N) (m ⊗ₜ[R] n) (m ⊗ₜ[R] n)
neg : i' = i → ¬k' = k → Eq (α := M ⊗[R] N) 0 (m ⊗ₜ[R] 0)
pos₁ : ¬i' = i → k' = k → Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] n)
⊢ 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)
have neg₁ : ¬i' = i → ¬k' = k → Eq (α := M ⊗[R] N) 0 (0 ⊗ₜ[R] 0)
Tactic: split_ifs
-- 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
⊢ 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) ((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)
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
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)
⊢ 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', k') = (i, k) then m ⊗ₜ[R] n 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
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)
⊢ 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 ∧ k' = k then m ⊗ₜ[R] n 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