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 ι
p : ι →₀ M
n : N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (p ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
have rw₁ : Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : M) ↦ (Finsupp.single a₁ (b ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
  ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
Tactic: rw [finsuppLeft_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
rw₁ :
  Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : M) ↦ (Finsupp.single a₁ (b ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (p ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
have rw₂ : Eq (α := M ⊗[R] N)
  (((Finsupp.single i ((p : (a : ι) → M) i ⊗ₜ[R] n) : ι →₀ M ⊗[R] N) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
  ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
Tactic: rw [finsuppLeft_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
p : ι →₀ M
n : N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (m : M) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
rw₁ :
  Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : M) ↦ (Finsupp.single a₁ (b ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
rw₂ :
  Eq (α := M ⊗[R] N)
    (((Finsupp.single i ((p : (a : ι) → M) i ⊗ₜ[R] n) : ι →₀ M ⊗[R] N) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (p ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
have rw₃ : Eq (α := M ⊗[R] N) ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N) ((p : (a : ι) → M) i ⊗ₜ[R] n : M ⊗[R] N)
Tactic: rw [finsuppLeft_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
t : (ι →₀ M) ⊗[R] N
i : ι
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft 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)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
have zero : Eq (α := M ⊗[R] N)
  ((((finsuppLeft 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)
  ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)
Tactic: induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_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 ι
t : (ι →₀ M) ⊗[R] N
i : ι
zero :
  Eq (α := M ⊗[R] N)
    ((((finsuppLeft 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)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft 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)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) t : M ⊗[R] N)
have tmul : ∀ (f : ι →₀ M) (n : N),
  Eq (α := M ⊗[R] N)
    (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
              (f ⊗ₜ[R] n) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (f ⊗ₜ[R] n) : M ⊗[R] N)
Tactic: induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_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 ι
t : (ι →₀ M) ⊗[R] N
i : ι
zero :
  Eq (α := M ⊗[R] N)
    ((((finsuppLeft 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)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) 0 : M ⊗[R] N)
tmul :
  ∀ (f : ι →₀ M) (n : N),
    Eq (α := M ⊗[R] N)
      (((((finsuppLeft R S M N ι : (ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N) : (a : (ι →₀ M) ⊗[R] N) → ι →₀ M ⊗[R] N)
                (f ⊗ₜ[R] n) :
              ι →₀ M ⊗[R] N) :
            (a : ι) → M ⊗[R] N)
          i :
        M ⊗[R] N)
      ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (f ⊗ₜ[R] n) : M ⊗[R] N)
⊢ Eq (α := M ⊗[R] N)
    (((((finsuppLeft 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)
    ((rTensor N (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)
      (((((finsuppLeft 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)
      ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) x : M ⊗[R] N))
  (hy :
    Eq (α := M ⊗[R] N)
      (((((finsuppLeft 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)
      ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) y : M ⊗[R] N)),
  Eq (α := M ⊗[R] N)
    (((((finsuppLeft 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)
    ((rTensor N (Finsupp.lapply i) : (a : (ι →₀ M) ⊗[R] N) → M ⊗[R] N) (x + y) : M ⊗[R] N)
Tactic: induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_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 ι
m : M
p : ι →₀ 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] p) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have zero : 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] 0) :
    ι →₀ M ⊗[R] N)
  (Finsupp.sum 0 fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
Tactic: induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]
Cleared hypotheses: p
-- 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 ι
m : M
p : ι →₀ N
zero :
  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] 0) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ 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)
        (m ⊗ₜ[R] p) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have add : ∀ (f g : ι →₀ N)
  (hf :
    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)
      (f.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N))
  (hg :
    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] g) :
        ι →₀ M ⊗[R] N)
      (g.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ 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)
        (m ⊗ₜ[R] (f + g)) :
      ι →₀ M ⊗[R] N)
    ((f + g).sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
Tactic: induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]
Cleared hypotheses: p
-- 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 ι
m : M
p : ι →₀ N
zero :
  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] 0) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum 0 fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
add :
  ∀ (f g : ι →₀ N)
    (hf :
      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)
        (f.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N))
    (hg :
      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] g) :
          ι →₀ M ⊗[R] N)
        (g.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ 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)
          (m ⊗ₜ[R] (f + g)) :
        ι →₀ M ⊗[R] N)
      ((f + g).sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ 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)
        (m ⊗ₜ[R] p) :
      ι →₀ M ⊗[R] N)
    (p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
have single : ∀ (a : ι) (b : 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 a b) :
      ι →₀ M ⊗[R] N)
    (Finsupp.sum (Finsupp.single a b) fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : ι →₀ M ⊗[R] N)
Tactic: induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]
Cleared hypotheses: p
-- 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 ι
m : M
p : ι →₀ N
i : ι
⊢ 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] p) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
have rw : Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
  (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
Tactic: rw [finsuppRight_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
p : ι →₀ N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : 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)
              (m ⊗ₜ[R] p) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
have rw₁ : Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : N) ↦ (Finsupp.single a₁ (m ⊗ₜ[R] b) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
  (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
Tactic: rw [finsuppRight_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
p : ι →₀ N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
rw₁ :
  Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : N) ↦ (Finsupp.single a₁ (m ⊗ₜ[R] b) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : 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)
              (m ⊗ₜ[R] p) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
have rw₂ : Eq (α := M ⊗[R] N)
  (((Finsupp.single i (m ⊗ₜ[R] (p : (a : ι) → N) i) : ι →₀ M ⊗[R] N) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
  (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
Tactic: rw [finsuppRight_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
m : M
p : ι →₀ N
i : ι
rw :
  Eq (α := M ⊗[R] N) ((p.sum fun (i : ι) (n : N) ↦ Finsupp.single i (m ⊗ₜ[R] n) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
rw₁ :
  Eq (α := M ⊗[R] N) (p.sum fun (a₁ : ι) (b : N) ↦ (Finsupp.single a₁ (m ⊗ₜ[R] b) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
rw₂ :
  Eq (α := M ⊗[R] N)
    (((Finsupp.single i (m ⊗ₜ[R] (p : (a : ι) → N) i) : ι →₀ M ⊗[R] N) : (a : ι) → M ⊗[R] N) i : M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : 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)
              (m ⊗ₜ[R] p) :
            ι →₀ M ⊗[R] N) :
          (a : ι) → M ⊗[R] N)
        i :
      M ⊗[R] N)
    (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
have rw₃ : Eq (α := M ⊗[R] N) (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N) (m ⊗ₜ[R] (p : (a : ι) → N) i : M ⊗[R] N)
Tactic: rw [finsuppRight_apply_tmul, 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
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
ι : Type u_5
inst_9 : DecidableEq ι
t : M ⊗[R] (ι →₀ N)
i : ι
⊢ 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 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)
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 ι
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)
⊢ 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 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)
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