awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
this : ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n
⊢ Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.Icc 1 n).finsuppAntidiag n) p.toFinsuppAntidiag

Tactic:
simpa [toFinsuppAntidiag, hp]

Premises used: Nat.Partition.toFinsuppAntidiag
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
suffices : ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n
⊢ Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.Icc 1 n).finsuppAntidiag n) p.toFinsuppAntidiag

Tactic:
suffices ∑ m ∈ Finset.Icc 1 n, Multiset.count m p.parts * m = n by simpa [toFinsuppAntidiag, hp]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ p.parts.sum = n

Tactic:
p.parts_sum

Premises used: Nat.Partition.parts_sum
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
h : p.parts.sum = ∑ m ∈ Finset.Icc 1 n, count m p.parts * m
⊢ ∑ m ∈ Finset.Icc 1 n, count m p.parts * m = n

Tactic:
convert! ← p.parts_sum

Premises used: Nat.Partition.parts_sum
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
h : Eq (α := ℕ) (∑ m ∈ p.parts.toFinset, count m p.parts • m) (∑ m ∈ Finset.Icc 1 n, count m p.parts * m)
⊢ p.parts.sum = ∑ m ∈ Finset.Icc 1 n, count m p.parts * m

Tactic:
rw [Finset.sum_multiset_count]

Premises used: Finset.sum_multiset_count
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
h : ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0
⊢ Eq (α := ℕ) (∑ m ∈ p.parts.toFinset, count m p.parts • m) (∑ m ∈ Finset.Icc 1 n, count m p.parts * m)

Tactic:
apply Finset.sum_subset hp

Premises used: Finset.sum_subset
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
this : ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0
⊢ ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
h : ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0
⊢ ∀ x ∈ Finset.Icc 1 n, x ∉ p.parts.toFinset → count x p.parts • x = 0

Tactic:
suffices ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0 by simpa
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
p : n.Partition
hp : p.parts.toFinset ⊆ Finset.Icc 1 n
⊢ ∀ (x : ℕ), 1 ≤ x → x ≤ n → x ∉ p.parts → x ∉ p.parts ∨ x = 0

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
hn : n ≠ 0
⊢ (indiscrete n).parts = {n}

Tactic:
simp [indiscrete, filter_eq_self, hn]

Premises used: Multiset.filter_eq_self, Nat.Partition.indiscrete
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
p : Partition 0
⊢ p.parts = 0

Tactic:
eq_zero_of_forall_notMem fun _ h => (p.parts_pos h).ne' <| sum_eq_zero_iff.1 p.parts_sum _ h

Premises used: LT.lt.ne', Iff.mp, Nat.Partition.parts_pos, Nat.Partition.parts_sum, Multiset.eq_zero_of_forall_notMem, Multiset.sum_eq_zero_iff
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
x : Partition 0
⊢ x.parts = parts (n := 0) default

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
p : Partition 1
⊢ p.parts = replicate p.parts.card 1

Tactic:
have h : p.parts = replicate (card p.parts) 1 := eq_replicate_card.2 fun x hx =>
    ((le_sum_of_mem hx).trans_eq p.parts_sum).antisymm (p.parts_pos hx)
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts.card = 1

Tactic:
simpa using (congrArg sum h.symm).trans p.parts_sum

Premises used: Multiset.sum, congrArg, Nat.Partition.parts_sum, Eq.symm, Eq.trans
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
⊢ p.parts.card = 1

Tactic:
have h' : card p.parts = 1 := by simpa using (congrArg sum h.symm).trans p.parts_sum
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
p : Partition 1
h : p.parts = replicate p.parts.card 1
h' : p.parts.card = 1
rw : Eq (α := Multiset ℕ) (replicate p.parts.card 1) {1}
rw₁ : Eq (α := Multiset ℕ) (replicate 1 1) {1}
rw₂ rw₃ : Eq (α := Multiset ℕ) {1} {1}
⊢ p.parts = {1}

Tactic:
rw [h, h', replicate_one]

Premises used: Multiset.replicate_one
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
σ : Type u_1
τ : Type u_2
inst : DecidableEq σ
inst_1 : DecidableEq τ
x : Partition 1
⊢ x.parts = parts (n := 1) default

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
σ : Type u_1
inst : DecidableEq σ
s : Sym σ 1
parts : ∀ (a : ℕ), count a (ofSym s).parts = count a (Partition.parts (n := 1) (indiscrete 1))
⊢ ofSym s = indiscrete 1

Tactic:
ext
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
σ : Type u_1
inst : DecidableEq σ
s : Sym σ 1
a : ℕ
⊢ count a (ofSym s).parts = count a (parts (n := 1) (indiscrete 1))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
i : ℕ
hi : i ≠ 0
⊢ count i (ofSums n l hl).parts = count i l

Tactic:
count_filter_of_pos hi

Premises used: Multiset.count_filter_of_pos, Multiset.filter
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
l : Multiset ℕ
hl : l.sum = n
⊢ count 0 (ofSums n l hl).parts = 0

Tactic:
count_filter_of_neg fun h => h rfl

Premises used: Multiset.count_filter_of_neg, rfl, Multiset.filter
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
congrm : ∀ (x : n.Partition), (∀ i ∈ x.parts, count i x.parts < 2) ↔ x.parts.Nodup
⊢ countRestricted n 2 = distincts n

Tactic:
congrm Finset.univ.filter fun x ↦ ?_

Premises used: Finset.univ, Finset.filter
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
x : n.Partition
rw : (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ x.parts.Nodup

Tactic:
rw [Multiset.nodup_iff_count_le_one]

Premises used: Multiset.nodup_iff_count_le_one
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Basic
Goal:
n : ℕ
x : n.Partition
⊢ (∀ i ∈ x.parts, count i x.parts < 2) ↔ ∀ (a : ℕ), count a x.parts ≤ 1

Tactic:
grind [Multiset.count_eq_zero]

Premises used: Multiset.count_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (genFun f) : R)
    (∑ p : n.Partition, Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) p.parts) f : R)

Tactic:
PowerSeries.coeff_mk _ _

Premises used: PowerSeries.coeff_mk, Nat.Partition.genFun
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (β := ℕ∞) (fun (j : ℕ) ↦ (f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))).order)
    Filter.atTop (nhds ⊤)

Tactic:
ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)

Premises used: Iff.mpr, Exists.intro, ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i : ℕ
refine : ∀ (n b : ℕ), b ≥ n → (↑n : ℕ∞) < (f (i + 1) (b + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1))).order
⊢ Filter.Tendsto (β := ℕ∞) (fun (j : ℕ) ↦ (f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))).order)
    Filter.atTop (nhds ⊤)

Tactic:
refine ENat.tendsto_nhds_top_iff_natCast_lt.mpr (fun n ↦ Filter.eventually_atTop.mpr ⟨n, ?_⟩)

Premises used: Iff.mpr, Exists.intro, ENat.tendsto_nhds_top_iff_natCast_lt, Filter.eventually_atTop
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
grw :
  (↑n : ℕ∞) <
    order.{u_1} (R := R) ((C : (a : R) → R⟦X⟧) (f (i + 1) (m + 1))) +
      (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
⊢ (↑n : ℕ∞) < (f (i + 1) (m + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order

Tactic:
grw [PowerSeries.smul_eq_C_mul, ← le_order_mul]

Premises used: PowerSeries.le_order_mul, PowerSeries.smul_eq_C_mul
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
⊢ 0 ≤ order.{u_1} (R := R) ((C : (a : R) → R⟦X⟧) (f (i + 1) (m + 1)))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
refine : (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order
⊢ (↑n : ℕ∞) <
    order.{u_1} (R := R) ((C : (a : R) → R⟦X⟧) (f (i + 1) (m + 1))) +
      (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order

Tactic:
refine lt_add_of_nonneg_of_lt (by simp) ?_

Premises used: lt_add_of_nonneg_of_lt
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
⊢ Nontrivial R

Tactic:
nontriviality R using Subsingleton.eq_zero

Premises used: Subsingleton.eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
h : Nontrivial R
rw : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑((i + 1) * (m + 1)) : ℕ∞)
⊢ (↑n : ℕ∞) < (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (m + 1))).order

Tactic:
rw [order_X_pow]

Premises used: PowerSeries.order_X_pow
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
h : Nontrivial R
norm_cast : n < (i + 1) * (m + 1)
⊢ LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑((i + 1) * (m + 1)) : ℕ∞)

Tactic:
norm_cast
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : m ≥ n
h : Nontrivial R
⊢ n < (i + 1) * (m + 1)

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
h :
  Filter.Tendsto (β := ℕ∞) (fun (i_1 : ℕ) ↦ (f (i + 1) (i_1 + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (i_1 + 1))).order)
    Filter.atTop (nhds ⊤)
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))

Tactic:
apply WithPiTopology.summable_of_tendsto_order_atTop_nhds_top

Premises used: PowerSeries.WithPiTopology.summable_of_tendsto_order_atTop_nhds_top
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
⊢ Filter.Tendsto (β := ℕ∞) (fun (i_1 : ℕ) ↦ (f (i + 1) (i_1 + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (i_1 + 1))).order)
    Filter.atTop (nhds ⊤)

Tactic:
apply tendsto_order_genFun_term_atTop_nhds_top

Premises used: Nat.Partition.tendsto_order_genFun_term_atTop_nhds_top
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
f : ℕ → ℕ → R
i : ℕ
hi : i ≠ 0
obtain :
  ∀ (a : ℕ) (hi : a + 1 ≠ 0),
    Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f (a + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((a + 1) * (j + 1))
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))

Tactic:
obtain ⟨a, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hi

Premises used: Nat.exists_eq_add_one_of_ne_zero, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
f : ℕ → ℕ → R
a : ℕ
hi : a + 1 ≠ 0
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (j : ℕ) ↦ f (a + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((a + 1) * (j + 1))

Tactic:
apply summable_genFun_term

Premises used: Nat.Partition.summable_genFun_term
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
hprod :
  ∀ i ∈ s,
    Ne (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))) :
        R)
      (0 : R)
x : ℕ
pos : ∀ (hx : x ∈ s), x ∣ (g : (a : ℕ) → ℕ) x
neg : ∀ (hx : x ∉ s), x ∣ (g : (a : ℕ) → ℕ) x
⊢ x ∣ (g : (a : ℕ) → ℕ) x

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
hprod :
  ∀ i ∈ s,
    Ne (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))) :
        R)
      (0 : R)
x : ℕ
hx : x ∈ s
⊢ Ne (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)

Tactic:
specialize hprod x hx
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod :
  Ne (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)
pos :
  ∀ (hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x),
    Eq (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
        R)
      (0 : R)
⊢ x ∣ (g : (a : ℕ) → ℕ) x

Tactic:
contrapose hprod
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
⊢ x ≠ 0

Tactic:
have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx)
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
pos :
  HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    0
⊢ Eq (α := R)
    ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1)))) :
      R)
    (0 : R)

Tactic:
rw [map_add, (summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)]

Premises used: PowerSeries.WithPiTopology.continuous_coeff, Summable.map_tsum, map_add, Nat.Partition.summable_genFun_term'
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
⊢ 0 = HAdd.hAdd (α := R) 0 (∑' (i : ℕ), 0)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
pos :
  HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    HAdd.hAdd (α := R) 0 (∑' (i : ℕ), 0)
⊢ HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    0

Tactic:
rw [show (0 : R) = 0 + ∑' (i : ℕ), 0 by simp]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
pos : Eq.{u_1 + 1} (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R) (0 : R)
pos₁ :
  ∀ (i : ℕ),
    Eq (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R) (0 : R)
⊢ HAdd.hAdd (α := R) (β := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i : ℕ),
          (coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) :
        R) =
    HAdd.hAdd (α := R) 0 (∑' (i : ℕ), 0)

Tactic:
congrm (?_ + ∑' (i : ℕ), ?_)

Premises used: HAdd.hAdd, tsum, SummationFilter.unconditional
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
this : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ Eq.{u_1 + 1} (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R) (0 : R)

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
pos : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ Eq.{u_1 + 1} (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) 1 : R) (0 : R)

Tactic:
suffices g x ≠ 0 by simp [this]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
pos : ∀ (hprod : Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)), x ∣ (g : (a : ℕ) → ℕ) x
⊢ Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
contrapose hprod
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hx0 : x ≠ 0
hprod : Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∣ (g : (a : ℕ) → ℕ) x

Tactic:
simp [hprod]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
pos : HSMul.hSMul (β := R) (f x (i + 1)) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) = 0
⊢ Eq (α := R) ((coeff ((g : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)
    (0 : R)

Tactic:
rw [map_smul, coeff_X_pow]

Premises used: PowerSeries.coeff_X_pow, map_smul
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
pos : Eq.{u_1 + 1} (α := R) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) 0
⊢ HSMul.hSMul (β := R) (f x (i + 1)) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) = 0

Tactic:
apply smul_eq_zero_of_right

Premises used: smul_eq_zero_of_right
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
this : (g : (a : ℕ) → ℕ) x ≠ x * (i + 1)
⊢ Eq.{u_1 + 1} (α := R) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) 0

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
pos : (g : (a : ℕ) → ℕ) x ≠ x * (i + 1)
⊢ Eq.{u_1 + 1} (α := R) (if (g : (a : ℕ) → ℕ) x = x * (i + 1) then 1 else 0) 0

Tactic:
suffices g x ≠ x * (i + 1) by simp [this]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ (g : (a : ℕ) → ℕ) x
hx0 : x ≠ 0
i : ℕ
pos : ∀ (hprod : (g : (a : ℕ) → ℕ) x = x * (i + 1)), x ∣ (g : (a : ℕ) → ℕ) x
⊢ (g : (a : ℕ) → ℕ) x ≠ x * (i + 1)

Tactic:
contrapose hprod
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
x : ℕ
hx : x ∈ s
hx0 : x ≠ 0
i : ℕ
hprod : (g : (a : ℕ) → ℕ) x = x * (i + 1)
⊢ x ∣ (g : (a : ℕ) → ℕ) x

Tactic:
simp [hprod]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
hprod :
  ∀ i ∈ s,
    Ne (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))) :
        R)
      (0 : R)
x : ℕ
hx : x ∉ s
this : Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∣ (g : (a : ℕ) → ℕ) x

Tactic:
simp [this]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) (s.finsuppAntidiag d) g
hprod :
  ∀ i ∈ s,
    Ne (α := R)
      ((coeff ((g : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))) :
        R)
      (0 : R)
x : ℕ
hx : x ∉ s
neg : Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∣ (g : (a : ℕ) → ℕ) x

Tactic:
suffices g x = 0 by simp [this]