awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
s_1 : Multiset M
a_1 : α
a : M
s : Multiset M
ih : Eq (α := α →₀ M) (single a_1 s.sum) (Multiset.sum (Multiset.map (single a_1) s))
rw : Eq (α := α →₀ M) (single a_1 (a + s.sum)) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
rw₁ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (single a_1 s.sum) = Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
rw₂ :
  HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s)) =
    Multiset.sum (Multiset.map (single a_1) (a ::ₘ s))
rw₃ :
  HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s)) =
    Multiset.sum (single a_1 a ::ₘ Multiset.map (single a_1) s)
⊢ Eq (α := α →₀ M) (single a_1 (a ::ₘ s).sum) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))
have rw₄ : HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s)) =
  HAdd.hAdd (α := α →₀ M) (single a_1 a) (Multiset.sum (Multiset.map (single a_1) s))
Tactic: rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
inst : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ Eq (α := α →₀ M) (single a (∑ b ∈ s, f b)) (∑ b ∈ s, single a (f b))
have trans : Eq (α := α →₀ M) (single a (∑ b ∈ s, f b))
  (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
Tactic: trans
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
inst : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
trans :
  Eq (α := α →₀ M) (single a (∑ b ∈ s, f b))
    (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
⊢ Eq (α := α →₀ M) (single a (∑ b ∈ s, f b)) (∑ b ∈ s, single a (f b))
have trans₁ : Eq (α := α →₀ M) (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
  (∑ b ∈ s, single a (f b))
Tactic: trans
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
inst : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
trans :
  Eq (α := α →₀ M) (single a (∑ b ∈ s, f b))
    (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
trans₁ :
  Eq (α := α →₀ M) (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
    (∑ b ∈ s, single a (f b))
⊢ Eq (α := α →₀ M) (single a (∑ b ∈ s, f b)) (∑ b ∈ s, single a (f b))
have trans₂ : α →₀ M
Tactic: trans
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
inst : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
⊢ Eq (α := α →₀ M) (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
    (∑ b ∈ s, single a (f b))
have rw : Eq (α := α →₀ M) (Multiset.sum (Multiset.map (single a ∘ fun (b : ι) ↦ f b) s.val)) (∑ b ∈ s, single a (f b))
Tactic: rw [Multiset.map_map]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : DecidableEq β
inst_1 : Zero M
inst_2 : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ (f.sum g).support ⊆ f.support.biUnion fun (a : α) ↦ (g a ((f : (a : α) → M) a)).support
have this : ∀ (c : β),
  Ne.{u_10 + 1} (α := N) (f.sum fun (a : α) (b : M) ↦ (g a b : (a : β) → N) c) 0 →
    ∃ (a : α),
      Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) ∧
        ¬Eq.{u_10 + 1} (α := N) ((g a ((f : (a : α) → M) a) : (a : β) → N) c : N) (0 : N)
Tactic: have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
    let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨a, mem_support_iff.mp ha, ne⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
inst : DecidableEq β
inst_1 : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.biUnion fun (x : α) ↦ (f x).support
have rw : (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support
Tactic: rw [← Finset.sup_eq_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β →₀ M
a : α
s : Finset α
h : a ∉ s
ih : (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support
⊢ ((cons a s h).sum f).support ⊆ (cons a s h).sup fun (x : α) ↦ (f x).support
have cons : (f a + ∑ x ∈ s, f x).support ⊆ (f a).support ⊔ s.sup fun (x : α) ↦ (f x).support
Tactic: rw [Finset.sum_cons, Finset.sup_cons]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
inst : DecidableEq β
inst_1 : AddCommMonoid M
s : Finset α
f : α → β →₀ M
⊢ (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support
have empty : (Finset.sum ∅ f).support ⊆ (Finset.sum ∅ f).support
Tactic: induction s using Finset.cons_induction_on with
  | empty => rfl
  | cons _ _ _ ih =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
inst : DecidableEq β
inst_1 : AddCommMonoid M
s : Finset α
f : α → β →₀ M
empty : (Finset.sum ∅ f).support ⊆ (Finset.sum ∅ f).support
⊢ (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support
have cons : ∀ (a : α) (s : Finset α) (h : a ∉ s) (ih : (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support),
  ((cons a s h).sum f).support ⊆ (cons a s h).sup fun (x : α) ↦ (f x).support
Tactic: induction s using Finset.cons_induction_on with
  | empty => rfl
  | cons _ _ _ ih =>
    rw [Finset.sum_cons, Finset.sup_cons]
    exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1
have refine_1 : ∀ (h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1), ∃ (a : α), d = single a 1
Tactic: refine ⟨fun h1 ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
refine_1 : ∀ (h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1), ∃ (a : α), d = single a 1
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1
have refine_2 : (∃ (a : α), d = single a 1) → Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
Tactic: refine ⟨fun h1 ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
⊢ ∃ (a : α), d = single a 1
have hd0 : d ≠ 0
Tactic: have hd0 : d ≠ 0 := (by simp [·] at h1)
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
⊢ ∃ (a : α), d = single a 1
have refine_1 : ∀ (a : α) (ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)), ∃ (a : α), d = single a 1
Tactic: obtain ⟨a, ha⟩ := ne_iff.mp hd0
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ) ∧ ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
have h1₁ : ¬(Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (0 : ℕ) ∧ Eq (α := ℕ) ((erase a d).sum fun (x : α) (n : ℕ) ↦ n) 1) →
  Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ) ∧ Eq (α := ℕ) ((erase a d).sum fun (x : α) (n : ℕ) ↦ n) 0
Tactic: rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
Cleared hypotheses: h1, ha
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
⊢ ∃ (a : α), d = single a 1
have hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
Tactic: obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
⊢ ∃ (a : α), d = single a 1
have hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
Tactic: obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∃ (a : α), d = single a 1
have h : d = single a 1
Tactic: use a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
⊢ d = single a 1
have h : ∀ (b : α), Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
b : α
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
have pos : ∀ (hb : b = a), Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
Tactic: by_cases hb : b = a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
b : α
pos : ∀ (hb : b = a), Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
have neg : ∀ (hb : ¬b = a), Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
Tactic: by_cases hb : b = a
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
b : α
hb : b = a
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
have pos : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
Tactic: rw [hb, single_eq_same, hda]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
a : α
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
hda : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
hda' : ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)
b : α
hb : b = a
pos : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((single a 1 : (a : α) → ℕ) a : ℕ)
pos₁ : Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ)
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
have pos₂ : Eq (α := ℕ) 1 1
Tactic: rw [hb, single_eq_same, hda]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
a : α
⊢ Eq (α := ℕ) (sum (single a 1) fun (x : α) (n : ℕ) ↦ n) 1
have rw : ∀ (b : α),
  Ne (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ) →
    b ≠ a → Eq (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ)
Tactic: rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1
have refine_1 : ∀ (h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1), ∃ (a : α), d = single a 1
Tactic: classical
  refine ⟨fun h1 ↦ ?_, ?_⟩
  · have hd0 : d ≠ 0 := (by simp [·] at h1)
    obtain ⟨a, ha⟩ := ne_iff.mp hd0
    obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]
    use a
    ext b
    by_cases hb : b = a
    · rw [hb, single_eq_same, hda]
    · simpa only [single_eq_of_ne hb] using hda' b hb
  · rintro ⟨a, rfl⟩
    rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]
    exact fun _ _ hba ↦ single_eq_of_ne hba
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
d : α →₀ ℕ
refine_1 : ∀ (h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1), ∃ (a : α), d = single a 1
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1
have refine_2 : (∃ (a : α), d = single a 1) → Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
Tactic: classical
  refine ⟨fun h1 ↦ ?_, ?_⟩
  · have hd0 : d ≠ 0 := (by simp [·] at h1)
    obtain ⟨a, ha⟩ := ne_iff.mp hd0
    obtain ⟨hda, hda'⟩ : d a = 1 ∧ ∀ i ≠ a, d i = 0 := by
      rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1
      simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]
    use a
    ext b
    by_cases hb : b = a
    · rw [hb, single_eq_same, hda]
    · simpa only [single_eq_of_ne hb] using hda' b hb
  · rintro ⟨a, rfl⟩
    rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]
    exact fun _ _ hba ↦ single_eq_of_ne hba
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : DecidableEq α
inst_1 : AddZeroClass M
inst_2 : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1
h_add : ∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h
have rw : Eq.{u_10 + 1} (α := N) (∏ x ∈ f.support ∪ g.support, h x ((f + g : (a : α) → M) x))
  (∏ x ∈ f.support ∪ g.support, h x ((f : (a : α) → M) x) * h x ((g : (a : α) → M) x))
Tactic: rw [Finsupp.prod_of_support_subset f subset_union_left h h_zero,
    Finsupp.prod_of_support_subset g subset_union_right h h_zero, ←
    Finset.prod_mul_distrib, Finsupp.prod_of_support_subset (f + g) Finsupp.support_add h h_zero]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F : α → M →+ N
⊢ (fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x))
      ((fun (F : α → M →+ N) ↦
          ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
            (α →₀ M) →+ N))
        F) =
    F
have h : ∀ (x : α) (x_1 : M),
  Eq.{u_10 + 1} (α := N)
    (((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x))
            ((fun (F : α → M →+ N) ↦
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := sorry,
                    map_add' := sorry } :
                  (α →₀ M) →+ N))
              F)
            x :
          (a : M) → N)
        x_1 :
      N)
    ((F x : (a : M) → N) x_1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F : (α →₀ M) →+ N
⊢ (fun (F : α → M →+ N) ↦
        ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
          (α →₀ M) →+ N))
      ((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x)) F) =
    F
have H₁ : ∀ (x : α) (x_1 : M),
  Eq.{u_10 + 1} (α := N)
    ((AddMonoidHom.comp
            ((fun (F : α → M →+ N) ↦
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := sorry,
                    map_add' := sorry } :
                  (α →₀ M) →+ N))
              ((fun (F : (α →₀ M) →+ N) (x : α) ↦ F.comp (singleAddHom x)) F))
            (singleAddHom x) :
          (a : M) → N)
        x_1 :
      N)
    ((F.comp (singleAddHom x) : (a : M) → N) x_1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
ι : Type u_2
γ : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
inst : AddCommMonoid A
inst_1 : AddCommMonoid B
inst_2 : AddCommMonoid C
t : ι → A → C
s : Finset α
f : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type u_7
M : Type u_8
M' : Type u_9
N : Type u_10
P : Type u_11
G_1 : Type u_12
H : Type u_13
R : Type u_14
S : Type u_15
inst_3 : AddZeroClass M
inst_4 : AddCommMonoid N
F G : α → M →+ N
⊢ { toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑((F + G) x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } =
    HAdd.hAdd (α := (α →₀ M) →+ N) (β := (α →₀ M) →+ N)
      ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
        (α →₀ M) →+ N)
      ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(G x) : (a : M) → N), map_zero' := ⋯, map_add' := ⋯ } :
        (α →₀ M) →+ N)
have H₁ : ∀ (x : α) (x_1 : M),
  Eq.{u_10 + 1} (α := N)
    ((AddMonoidHom.comp (N := α →₀ M)
            ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑((F + G) x) : (a : M) → N), map_zero' := sorry,
                map_add' := sorry } :
              (α →₀ M) →+ N)
            (singleAddHom x : M →+ α →₀ M) :
          (a : M) → N)
        x_1 :
      N)
    (((HAdd.hAdd (α := (α →₀ M) →+ N) (β := (α →₀ M) →+ N)
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(F x) : (a : M) → N), map_zero' := sorry,
                    map_add' := sorry } :
                  (α →₀ M) →+ N)
                ({ toFun := fun (f : α →₀ M) ↦ f.sum fun (x : α) ↦ (⇑(G x) : (a : M) → N), map_zero' := sorry,
                    map_add' := sorry } :
                  (α →₀ M) →+ N)).comp
            (singleAddHom x) :
          (a : M) → N)
        x_1 :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
⊢ ∑ a : α, single a ((f : (a : α) → M) a) = f
have refine : Eq (α := (a : α) → M)
  ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
  ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)
Tactic: refine DFunLike.coe_injective ?_
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
simp_rw simp_rw₁ : Eq (α := (a : α) → M) (⇑(∑ a : α, single a ((f : (a : α) → M) a)) : (a : α) → M) (⇑f : (a : α) → M)
⊢ Eq (α := (a : α) → M)
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)
have simp_rw₂ : Eq (α := (a : α) → M) (∑ i : α, (⇑(single i ((f : (a : α) → M) i) : α →₀ M) : (a : α) → M)) (⇑f : (a : α) → M)
Tactic: simp_rw [coe_finsetSum, single_eq_pi_single, Finset.univ_sum_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
simp_rw simp_rw₁ : Eq (α := (a : α) → M) (⇑(∑ a : α, single a ((f : (a : α) → M) a)) : (a : α) → M) (⇑f : (a : α) → M)
simp_rw₂ :
  Eq (α := (a : α) → M) (∑ i : α, (⇑(single i ((f : (a : α) → M) i) : α →₀ M) : (a : α) → M)) (⇑f : (a : α) → M)
⊢ Eq (α := (a : α) → M)
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
    ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)
have simp_rw₃ : Eq (α := (a : α) → M) (∑ x : α, Pi.single (M := fun (j : α) ↦ M) x ((f : (a : α) → M) x)) (⇑f : (a : α) → M)
Tactic: simp_rw [coe_finsetSum, single_eq_pi_single, Finset.univ_sum_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : Fintype α
inst_1 : AddCommMonoid M
f : α →₀ M
⊢ ∑ a : α, single a ((f : (a : α) → M) a) = f
have refine : Eq (α := (a : α) → M)
  ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) (∑ a : α, single a ((f : (a : α) → M) a)))
  ((fun (f : α →₀ M) ↦ ((⇑f : (a : α) → M) : (a : α) → M)) f)
Tactic: classical
  refine DFunLike.coe_injective ?_
  simp_rw [coe_finsetSum, single_eq_pi_single, Finset.univ_sum_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
⊢ ∑ j : α, (single i m : (a : α) → M) j = m
have rw : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
Tactic: rw [single, coe_mk, Finset.sum_pi_single']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
⊢ ∑ j : α, (single i m : (a : α) → M) j = m
have classical : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
Tactic: classical rw [single, coe_mk, Finset.sum_pi_single']
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
⊢ ∑ j : α, (single j m : (a : α) → M) i = m
have simp_rw : ∑ x : α, Pi.single (M := fun (a : α) ↦ M) x m i = m
Tactic: simp_rw [single, coe_mk]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single (M := fun (a : α) ↦ M) x m i = m
have rw : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
Tactic: rw [Finset.sum_pi_single]
-- Lean 4 proof step from Mathlib.Algebra.BigOperators.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_8
inst : AddCommMonoid M
inst_1 : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single (M := fun (a : α) ↦ M) x m i = m
have classical : (if Membership.mem (γ := Finset α) univ i then m else 0) = m
Tactic: classical rw [Finset.sum_pi_single]