awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
⊢ f.prod g = g a ((f : (a : α) → M) a)

Tactic:
Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)

Premises used: Finset.prod_eq_single, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
refine_1 : ∀ (b : α) (hb₁ : b ∈ f.support) (hb₂ : b ≠ a), g b ((f : (a : α) → M) b) = 1
refine_2 : ∀ (h : a ∉ f.support), g a ((f : (a : α) → M) a) = 1
⊢ f.prod g = g a ((f : (a : α) → M) a)

Tactic:
refine Finset.prod_eq_single a (fun b hb₁ hb₂ => ?_) (fun h => ?_)

Premises used: Finset.prod_eq_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
b : α
hb₁ : b ∈ f.support
hb₂ : b ≠ a
⊢ g b ((f : (a : α) → M) b) = 1

Tactic:
h₀ b (mem_support_iff.mp hb₁) hb₂

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
b : α
hb₁ : b ∈ f.support
hb₂ : b ≠ a
⊢ g b ((f : (a : α) → M) b) = 1

Tactic:
exact h₀ b (mem_support_iff.mp hb₁) hb₂

Premises used: Finsupp.mem_support_iff, Iff.mp
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
h : a ∉ f.support
⊢ Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)

Tactic:
simp only [notMem_support_iff] at h

Premises used: Finsupp.notMem_support_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
h : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
refine_2 : g a 0 = 1
⊢ g a ((f : (a : α) → M) a) = 1

Tactic:
rw [h]
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
h : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ g a 0 = 1

Tactic:
h₁ h
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
f : α →₀ M
a : α
g : α → M → N
h₀ : ∀ (b : α), Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) b : M) (0 : M) → b ≠ a → g b ((f : (a : α) → M) b) = 1
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → g a 0 = 1
h : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ g a 0 = 1

Tactic:
exact h₁ h
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : CommMonoid N
inst_2 : Unique α
f : α →₀ M
g : α → M → N
h₁ : Eq.{u_8 + 1} (α := M) ((f : (a : α) → M) default : M) (0 : M) → g default 0 = 1
a : α
⊢ Ne.{u_8 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M) → a ≠ default → g a ((f : (a : α) → M) a) = 1

Tactic:
simp [Subsingleton.elim a default]

Premises used: Inhabited.default, Subsingleton.elim
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
β : Type u_7
inst : Zero α
inst_1 : CommMonoidWithZero β
inst_2 : Nontrivial β
inst_3 : NoZeroDivisors β
f : ι →₀ α
g : ι → α → β
⊢ f.prod g = 0 ↔ ∃ i ∈ f.support, g i ((f : (a : ι) → α) i) = 0

Tactic:
Finset.prod_eq_zero_iff

Premises used: Finset.prod_eq_zero_iff, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
β : Type u_7
inst : Zero α
inst_1 : CommMonoidWithZero β
inst_2 : Nontrivial β
inst_3 : NoZeroDivisors β
f : ι →₀ α
g : ι → α → β
⊢ f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i ((f : (a : ι) → α) i) ≠ 0

Tactic:
Finset.prod_ne_zero_iff

Premises used: Finset.prod_ne_zero_iff, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
P : Type u_11
inst : Zero M
inst_1 : CommMonoid N
inst_2 : CommMonoid P
H : Type u_16
inst_3 : FunLike H N P
inst_4 : MonoidHomClass H N P
h : H
f : α →₀ M
g : α → M → N
⊢ Eq.{u_11 + 1} (α := P) ((h : (a : N) → P) (f.prod g) : P) (f.prod fun (a : α) (b : M) ↦ (h : (a : N) → P) (g a b) : P)

Tactic:
map_prod h _ _

Premises used: map_prod, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
N : Type u_10
P : Type u_11
inst : Zero β
inst_1 : MulOneClass N
inst_2 : CommMonoid P
f : α →₀ β
g : α → β → N →* P
⊢ Eq (α := (a : N) → P) (⇑(f.prod g) : (a : N) → P) (f.prod fun (i : α) (fi : β) ↦ (⇑(g i fi) : (a : N) → P))

Tactic:
MonoidHom.coe_finsetProd _ _

Premises used: MonoidHom.coe_finsetProd, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
N : Type u_10
P : Type u_11
inst : Zero β
inst_1 : MulOneClass N
inst_2 : CommMonoid P
f : α →₀ β
g : α → β → N →* P
x : N
⊢ Eq.{u_11 + 1} (α := P) ((f.prod g : (a : N) → P) x : P) (f.prod fun (i : α) (fi : β) ↦ (g i fi : (a : N) → P) x : P)

Tactic:
MonoidHom.finsetProd_apply _ _ _

Premises used: MonoidHom.finsetProd_apply, Finsupp.prod
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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)
rw₄ 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))
⊢ Eq (α := α →₀ M) (single a_1 (a ::ₘ s).sum) (Multiset.sum (Multiset.map (single a_1) (a ::ₘ s)))

Tactic:
rw [Multiset.sum_cons, single_add, ih, Multiset.map_cons, Multiset.sum_cons]

Premises used: Multiset.map_cons, Finsupp.single_add, Multiset.sum_cons
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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))
trans₂ : α →₀ M
⊢ Eq (α := α →₀ M) (single a (∑ b ∈ s, f b)) (∑ b ∈ s, single a (f b))

Tactic:
trans
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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))
    (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))

Tactic:
apply single_multiset_sum

Premises used: Finsupp.single_multiset_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
inst : AddCommMonoid M
s : Finset ι
f : ι → M
a : α
rw : Eq (α := α →₀ M) (Multiset.sum (Multiset.map (single a ∘ fun (b : ι) ↦ f b) s.val)) (∑ b ∈ s, single a (f b))
⊢ Eq (α := α →₀ M) (Multiset.sum (Multiset.map (single a) (Multiset.map (fun (b : ι) ↦ f b) s.val)))
    (∑ b ∈ s, single a (f b))

Tactic:
rw [Multiset.map_map]

Premises used: Multiset.map_map
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 ∘ fun (b : ι) ↦ f b) s.val)) (∑ b ∈ s, single a (f b))

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : AddCommMonoid N
s : ι →₀ M
f : ι → M → N
a : α
⊢ Eq (α := α →₀ N) (single a (s.sum f)) (s.sum fun (d : ι) (c : M) ↦ single a (f d c))

Tactic:
single_finsetSum _ _ _

Premises used: Finsupp.sum, Finsupp.single_finsetSum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
G : Type u_12
inst : SubtractionMonoid G
inst_1 : CommMonoid M
g : α →₀ G
h : α → G → M
h0 : ∀ (a : α), h a 0 = 1
⊢ (-g).prod h = g.prod fun (a : α) (b : G) ↦ h a (-b)

Tactic:
prod_mapRange_index h0

Premises used: Finsupp.prod_mapRange_index
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
N : Type u_10
inst : AddCommMonoid N
S : Finset ι
f : ι → α →₀ N
a : α
⊢ Eq.{u_10 + 1} (α := N) ((∑ i ∈ S, f i : (a : α) → N) a : N) (∑ i ∈ S, (f i : (a : α) → N) a : N)

Tactic:
map_sum (applyAddHom a) _ _

Premises used: Finsupp.applyAddHom, map_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
a₂ : β
⊢ Eq.{u_10 + 1} (α := N) ((f.sum g : (a : β) → N) a₂ : N) (f.sum fun (a₁ : α) (b : M) ↦ (g a₁ b : (a : β) → N) a₂ : N)

Tactic:
finsetSum_apply _ _ _

Premises used: Finsupp.sum, Finsupp.finsetSum_apply
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
ι : Type u_2
N : Type u_10
inst : AddCommMonoid N
S : Finset ι
f : ι → α →₀ N
⊢ Eq (α := (a : α) → N) (⇑(∑ i ∈ S, f i) : (a : α) → N) (∑ i ∈ S, (⇑(f i) : (a : α) → N))

Tactic:
map_sum (coeFnAddHom : (α →₀ N) →+ _) _ _

Premises used: Finsupp.coeFnAddHom, map_sum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ Eq (α := (a : β) → N) (⇑(f.sum g) : (a : β) → N) (f.sum fun (a₁ : α) (b : M) ↦ (⇑(g a₁ b) : (a : β) → N))

Tactic:
coe_finsetSum _ _

Premises used: Finsupp.sum, Finsupp.coe_finsetSum
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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
⊢ ∀ (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⟩
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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
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)
⊢ (f.sum g).support ⊆ f.support.biUnion fun (a : α) ↦ (g a ((f : (a : α) → M) a)).support

Tactic:
simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]

Premises used: Finsupp.mem_support_iff, exists_prop, Finset.subset_iff, Finsupp.sum_apply, Finset.mem_biUnion
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
inst : DecidableEq β
inst_1 : AddCommMonoid M
s : Finset α
f : α → β →₀ M
rw : (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support
⊢ (s.sum f).support ⊆ s.biUnion fun (x : α) ↦ (f x).support

Tactic:
rw [← Finset.sup_eq_biUnion]

Premises used: Finset.sup_eq_biUnion
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_7
M : Type u_8
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β →₀ M
⊢ (Finset.sum ∅ f).support ⊆ (Finset.sum ∅ f).support

Tactic:
rfl
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : (f a + ∑ x ∈ s, f x).support ⊆ (f a).support ⊔ s.sup fun (x : α) ↦ (f x).support
⊢ ((Finset.cons a s h).sum f).support ⊆ (Finset.cons a s h).sup fun (x : α) ↦ (f x).support

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]

Premises used: Finset.sum_cons, Finset.sup_cons
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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
⊢ (f a + ∑ x ∈ s, f x).support ⊆ (f a).support ⊔ s.sup fun (x : α) ↦ (f x).support

Tactic:
support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Premises used: Set.Mem, Finset.Subset.refl, setOf, Finset.union_subset_union, HasSubset.Subset.trans, Finsupp.support_add
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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
⊢ (f a + ∑ x ∈ s, f x).support ⊆ (f a).support ⊔ s.sup fun (x : α) ↦ (f x).support

Tactic:
exact support_add.trans (Finset.union_subset_union (Finset.Subset.refl _) ih)

Premises used: Finset.Subset.refl, Finset.union_subset_union, HasSubset.Subset.trans, Finsupp.support_add
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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
cons :
  ∀ (a : α) (s : Finset α) (h : a ∉ s) (ih : (s.sum f).support ⊆ s.sup fun (x : α) ↦ (f x).support),
    ((Finset.cons a s h).sum f).support ⊆ (Finset.cons a s h).sup fun (x : α) ↦ (f x).support
⊢ (s.sum f).support ⊆ s.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)

Premises used: Finset.sum_cons, Finset.cons, Finset.sup_cons
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_8
N : Type u_10
inst : Zero M
inst_1 : AddCommMonoid N
f : α →₀ M
⊢ Eq.{u_10 + 1} (α := N) (f.sum fun (x : α) (x_1 : M) ↦ 0) 0

Tactic:
Finset.sum_const_zero

Premises used: Finsupp.sum, Finset.sum_const_zero
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
d : α →₀ ℕ
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1

Tactic:
⟨fun h1 ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
d : α →₀ ℕ
refine_1 : ∀ (h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1), ∃ (a : α), d = single a 1
refine_2 : (∃ (a : α), d = single a 1) → Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
⊢ Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1 ↔ ∃ (a : α), d = single a 1

Tactic:
refine ⟨fun h1 ↦ ?_, ?_⟩
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
⊢ d ≠ 0

Tactic:
have hd0 : d ≠ 0 := (by simp [·] at h1)
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
d : α →₀ ℕ
h1 : Eq (α := ℕ) (d.sum fun (x : α) (n : ℕ) ↦ n) 1
hd0 : d ≠ 0
refine_1 : ∀ (a : α) (ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)), ∃ (a : α), d = single a 1
⊢ ∃ (a : α), d = single a 1

Tactic:
obtain ⟨a, ha⟩ := ne_iff.mp hd0

Premises used: Iff.mp, Finsupp.ne_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ) (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

Premises used: Finsupp.add_sum_erase', Classical.or_iff_not_imp_left, Nat.add_eq_one_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)
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
⊢ Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)

Tactic:
rw [← add_sum_erase' _ a _ (fun _ ↦ rfl), Nat.add_eq_one_iff, or_iff_not_imp_left] at h1

Premises used: Finsupp.add_sum_erase', Classical.or_iff_not_imp_left, Nat.add_eq_one_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
d : α →₀ ℕ
hd0 : d ≠ 0
a : α
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
ha : Ne (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) ((0 : (a : α) → ℕ) a : ℕ)
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) a : ℕ) (1 : ℕ) ∧ ∀ (i : α), i ≠ a → Eq (α := ℕ) ((d : (a : α) → ℕ) i : ℕ) (0 : ℕ)

Tactic:
simp_all +contextual [sum, support_erase, sum_eq_zero_iff, mem_erase, erase_ne]

Premises used: Finsupp.erase_ne, Finsupp.sum, Finsupp.support_erase, Finset.mem_erase, Finset.sum_eq_zero_iff
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)

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]

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)
⊢ ∀ (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]

Premises used: DFunLike.coe
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)
h : d = single a 1
⊢ ∃ (a : α), d = single a 1

Tactic:
use a
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)
h : ∀ (b : α), Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
⊢ d = single a 1

Tactic:
ext b
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)
neg : ∀ (hb : ¬b = a), Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)

Tactic:
by_cases hb : b = a
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)
pos₂ pos₃ : Eq (α := ℕ) 1 1
⊢ Eq (α := ℕ) ((d : (a : α) → ℕ) b : ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ)

Tactic:
rw [hb, single_eq_same, hda]

Premises used: Finsupp.single_eq_same
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
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 : ℕ)

Tactic:
simpa only [single_eq_of_ne hb] using hda' b hb

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
a : α
rw :
  ∀ (b : α),
    Ne (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ) →
      b ≠ a → Eq (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (sum (single a 1) fun (x : α) (n : ℕ) ↦ n) 1

Tactic:
rw [sum_eq_single a ?_ (fun _ ↦ rfl), single_eq_same]

Premises used: Finsupp.single_eq_same, Finsupp.sum_eq_single
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
a : α
⊢ ∀ (b : α),
    Ne (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ) →
      b ≠ a → Eq (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ)

Tactic:
fun _ _ hba ↦ single_eq_of_ne hba

Premises used: Finsupp.single_eq_of_ne
-- Module: Mathlib.Algebra.BigOperators.Finsupp.Basic
Goal:
α : Type u_1
a : α
⊢ ∀ (b : α),
    Ne (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ) →
      b ≠ a → Eq (α := ℕ) ((single a 1 : (a : α) → ℕ) b : ℕ) (0 : ℕ)

Tactic:
exact fun _ _ hba ↦ single_eq_of_ne hba

Premises used: Finsupp.single_eq_of_ne