awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst : Semiring R
inst_1 : Zero N
f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N
⊢ (fun (f : (i : ι) × η i →₀ N) ↦
        (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
            (Trunc.mk
              (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                f.splitSupport (αs := η).val ⋯)) :
          Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
      ((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
          (onFinset
              (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                ((f : (a : ι) → η a →₀ N) j).support)
              (fun (ji : (i : ι) × η i) ↦
                ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                  (ji.snd (β := fun (i : ι) ↦ η i)))
              ⋯ :
            (i : ι) × η i →₀ N))
        f) =
    f
have h : ∀ (i : ι) (a : η i),
  Eq.{u_5 + 1} (α := N)
    ((((fun (f : (i : ι) × η i →₀ N) ↦
                  (DFinsupp.mk' (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (f.split (αs := η))
                      (Trunc.mk
                        (Subtype.mk (p := fun (s : Multiset ι) ↦ ∀ (i : ι), i ∈ s ∨ f.split (αs := η) i = 0)
                          f.splitSupport (αs := η).val sorry)) :
                    Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N))
                ((fun (f : Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) ↦
                    (onFinset
                        (f.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N).sigma (α := η) fun (j : ι) ↦
                          ((f : (a : ι) → η a →₀ N) j).support)
                        (fun (ji : (i : ι) × η i) ↦
                          ((f : (a : ι) → η a →₀ N) (ji.fst (β := fun (i : ι) ↦ η i)) : (a : η ji.fst) → N)
                            (ji.snd (β := fun (i : ι) ↦ η i)))
                        sorry :
                      (i : ι) × η i →₀ N))
                  f) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
    (((f : (a : ι) → η a →₀ N) i : (a : η i) → N) a : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
inst_2 : (i : ι) → (x : Finsupp.{u_4, u_5} (η i) N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
⊢ DFinsupp.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f) =
    f.splitSupport (αs := η)
have h : ∀ (a : ι),
  Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
        ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f))
      a ↔
    a ∈ f.splitSupport (αs := η)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
inst_2 : (i : ι) → (x : Finsupp.{u_4, u_5} (η i) N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a : ι
⊢ Membership.mem (γ := Finset ι)
      (DFinsupp.support (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
        ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f))
      a ↔
    a ∈ f.splitSupport (αs := η)
have h : (((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
          Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
        (a : ι) → η a →₀ N)
      a ≠
    0 ↔
  a ∈ f.splitSupport (αs := η)
Tactic: rw [DFinsupp.mem_support_toFun]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
a : (i : ι) × η i
n : N
⊢ Eq (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (single a n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    (DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N) (a.fst (β := fun (i : ι) ↦ η i))
        (single (a.snd (β := fun (i : ι) ↦ η i)) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
have obtain : ∀ (i : ι) (a : η i),
  Eq (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
        (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    (DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
        ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
        (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
Tactic: obtain ⟨i, a⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
⊢ Eq (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
        (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
    (DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
        ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
        (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
      Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
have h : ∀ (j : ι) (b : η j),
  Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
Tactic: ext j b
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
have pos : ∀ (h : i = j),
  Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
pos :
  ∀ (h : i = j),
    Eq.{u_5 + 1} (α := N)
      (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                    (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
      (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                  ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                  (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
                (a : ι) → η a →₀ N)
              j :
            (a : η j) → N)
          b :
        N)
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
have neg : ∀ (h : ¬i = j),
  Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : i = j
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
have pos : ∀ (b : η i),
  Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        b :
      N)
Tactic: subst h
Cleared hypotheses: j, b, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N)
                  (single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
    (((DFinsupp.single (β := fun (i : ι) ↦ Finsupp.{u_4, u_5} (η i) N)
                ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).fst (β := fun (i : ι) ↦ η i))
                (single ((Sigma.mk (β := fun (i : ι) ↦ η i) i a).snd (β := fun (i : ι) ↦ η i)) n) :
              (a : ι) → η a →₀ N)
            j :
          (a : η j) → N)
        b :
      N)
have neg : Eq.{u_5 + 1} (α := N)
  ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
      (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
    N)
  (0 : N)
Tactic: suffices Finsupp.single (⟨i, a⟩ : Σ i, η i) n ⟨j, b⟩ = 0 by simp [split_apply, dif_neg h, this]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (hypothesis)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
have H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
Tactic: have H : (⟨i, a⟩ : Σ i, η i) ≠ ⟨j, b⟩ := by simp [h]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
have neg : (if Sigma.mk (β := fun (i : ι) ↦ η i) i a = Sigma.mk (β := fun (i : ι) ↦ η i) j b then n else 0) = 0
Tactic: rw [Finsupp.single_apply, if_neg H]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
neg : (if Sigma.mk (β := fun (i : ι) ↦ η i) i a = Sigma.mk (β := fun (i : ι) ↦ η i) j b then n else 0) = 0
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
have neg₁ : Eq.{u_5 + 1} (α := N) 0 0
Tactic: rw [Finsupp.single_apply, if_neg H]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
have neg : (if Sigma.mk (β := fun (i : ι) ↦ η i) i a = Sigma.mk (β := fun (i : ι) ↦ η i) j b then n else 0) = 0
Tactic: classical rw [Finsupp.single_apply, if_neg H]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : DecidableEq ι
inst_1 : Zero N
n : N
i : ι
a : η i
j : ι
b : η j
h : ¬i = j
H : Sigma.mk (β := fun (i : ι) ↦ η i) i a ≠ Sigma.mk (β := fun (i : ι) ↦ η i) j b
neg : (if Sigma.mk (β := fun (i : ι) ↦ η i) i a = Sigma.mk (β := fun (i : ι) ↦ η i) j b then n else 0) = 0
⊢ Eq.{u_5 + 1} (α := N)
    ((single (Sigma.mk (β := fun (i : ι) ↦ η i) i a) n : (a : (i : ι) × η i) → N)
        (Sigma.mk (β := fun (i : ι) ↦ η i) j b) :
      N)
    (0 : N)
have neg₁ : Eq.{u_5 + 1} (α := N) 0 0
Tactic: classical rw [Finsupp.single_apply, if_neg H]
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ (sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (f + g) =
    HAdd.hAdd (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) g :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
have h : ∀ (i : ι) (a : η i),
  Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (f + g) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
    (((HAdd.hAdd (α := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
                ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
                ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) g :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.ToDFinsupp (goal)
Goal:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst : Monoid R
inst_1 : AddMonoid N
inst_2 : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ (sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (r • f) =
    HSMul.hSMul (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) r
      ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
        Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N)
have h : ∀ (i : ι) (a : η i),
  Eq.{u_5 + 1} (α := N)
    (((((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) (r • f) :
                Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
    (((HSMul.hSMul (β := Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) r
                ((sigmaFinsuppEquivDFinsupp (η := η) : (a : (i : ι) × η i →₀ N) → Π₀ (i : ι), η i →₀ N) f :
                  Π₀ (i : ι), Finsupp.{u_4, u_5} (η i) N) :
              (a : ι) → η a →₀ N)
            i :
          (a : η i) → N)
        a :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : DecidableEq σ
s : σ
f : σ →₀ R
⊢ Eq.{u_3 + 1} (α := R) ((weight (Pi.single (M := fun (a : σ) ↦ R) s 1) : (a : σ →₀ R) → R) f : R)
    ((f : (a : σ) → R) s : R)
have rw : HSMul.hSMul (α := R) (β := R) ((f : (a : σ) → R) s : R) 1 = (f : (a : σ) → R) s
Tactic: rw [weight_single_index, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : DecidableEq σ
s : σ
f : σ →₀ R
rw : HSMul.hSMul (α := R) (β := R) ((f : (a : σ) → R) s : R) 1 = (f : (a : σ) → R) s
⊢ Eq.{u_3 + 1} (α := R) ((weight (Pi.single (M := fun (a : σ) ↦ R) s 1) : (a : σ →₀ R) → R) f : R)
    ((f : (a : σ) → R) s : R)
have rw₁ : HMul.hMul (α := R) (β := R) ((f : (a : σ) → R) s : R) (1 : R) = (f : (a : σ) → R) s
Tactic: rw [weight_single_index, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : Semiring R
inst_1 : DecidableEq σ
s : σ
f : σ →₀ R
rw : HSMul.hSMul (α := R) (β := R) ((f : (a : σ) → R) s : R) 1 = (f : (a : σ) → R) s
rw₁ : HMul.hMul (α := R) (β := R) ((f : (a : σ) → R) s : R) (1 : R) = (f : (a : σ) → R) s
⊢ Eq.{u_3 + 1} (α := R) ((weight (Pi.single (M := fun (a : σ) ↦ R) s 1) : (a : σ →₀ R) → R) f : R)
    ((f : (a : σ) → R) s : R)
have rw₂ : Eq.{u_3 + 1} (α := R) ((f : (a : σ) → R) s : R) ((f : (a : σ) → R) s : R)
Tactic: rw [weight_single_index, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
hw : ∀ (i : σ), w i ≠ 0
n : R
s : σ
h : n • w s = 0
⊢ n = 0
have h₁ : ¬w s = 0 → n = 0
Tactic: rw [smul_eq_zero, or_iff_not_imp_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (hypothesis)
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : NonTorsionWeight R w
s : σ
h : w s = 0
⊢ False
have h₁ : HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (w s) = 0
Tactic: rw [← one_smul R (w s)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
R : Type u_3
inst : Semiring R
w : σ → M
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
inst_4 : NonTorsionWeight R w
s : σ
h : HSMul.hSMul.{u_3, u_2, u_2} (α := R) 1 (w s) = 0
⊢ False
have apply : Eq.{u_3 + 1} (α := R) 1 0
Tactic: apply zero_ne_one.symm (α := R)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
| ((weight w : (a : σ →₀ ℕ) → M) f : M)
have rw : (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
Tactic: rw [← sub_add_single_one_cancel hi, weight_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) = (weight w : (a : σ →₀ ℕ) → M) f
have conv_rhs : HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) =
  (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
Tactic: conv_rhs => rw [← sub_add_single_one_cancel hi, weight_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
⊢ HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) =
    (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
have rw : HSMul.hSMul (α := ℕ) 0 (w i) = 0
Tactic: rw [sum_add_index', sum_single_index, one_smul, weight_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
rw : HSMul.hSMul (α := ℕ) 0 (w i) = 0
⊢ HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) =
    (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
have h_zero : ∀ (a : σ), HSMul.hSMul (α := ℕ) 0 (w a) = 0
Tactic: rw [sum_add_index', sum_single_index, one_smul, weight_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Weight (goal)
Goal:
σ : Type u_1
M : Type u_2
w : σ → M
inst : AddCommMonoid M
f : σ →₀ ℕ
i : σ
hi : Ne (α := ℕ) ((f : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
rw : HSMul.hSMul (α := ℕ) 0 (w i) = 0
h_zero : ∀ (a : σ), HSMul.hSMul (α := ℕ) 0 (w a) = 0
⊢ HAdd.hAdd (α := M) ((weight w : (a : σ →₀ ℕ) → M) (f - single i 1) : M) (w i) =
    (f - single i 1 + single i 1).sum fun (i : σ) (c : ℕ) ↦ c • w i
have h_add : ∀ (a : σ) (b₁ b₂ : ℕ), (b₁ + b₂) • w a = b₁ • w a + b₂ • w a
Tactic: rw [sum_add_index', sum_single_index, one_smul, weight_apply]