awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
h1 : s.sum (⇑g : (a : ℕ) → ℕ) = d
h2 : g.support ⊆ s
refine_3 :
  Eq (α := ℕ) (∑ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x) (∑ x ∈ s, (g : (a : ℕ) → ℕ) x)
⊢ Eq (α := ℕ)
    (Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }))
    (s.sum (⇑g : (a : ℕ) → ℕ))

Tactic:
suffices ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x by simpa [Finsupp.sum]
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
h1 : s.sum (⇑g : (a : ℕ) → ℕ) = d
h2 : g.support ⊆ s
⊢ ∀ x ∈ s \ g.support, Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (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
hprod :
  ∀ (i : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
h1 : s.sum (⇑g : (a : ℕ) → ℕ) = d
h2 : g.support ⊆ s
refine_3 : ∀ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x = (g : (a : ℕ) → ℕ) x
⊢ Eq (α := ℕ) (∑ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x) (∑ x ∈ s, (g : (a : ℕ) → ℕ) x)

Tactic:
apply sum_subset_zero_on_sdiff h2 (by simp)

Premises used: Finset.sum_subset_zero_on_sdiff
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
h1 : s.sum (⇑g : (a : ℕ) → ℕ) = d
h2 : g.support ⊆ s
⊢ ∀ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x = (g : (a : ℕ) → ℕ) x

Tactic:
fun x hx ↦ Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x

Premises used: _private.0.Nat.Partition.aux_dvd_of_coeff_ne_zero, Nat.div_mul_cancel
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
h1 : s.sum (⇑g : (a : ℕ) → ℕ) = d
h2 : g.support ⊆ s
⊢ ∀ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x = (g : (a : ℕ) → ℕ) x

Tactic:
exact fun x hx ↦ Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x

Premises used: _private.0.Nat.Partition.aux_dvd_of_coeff_ne_zero, Nat.div_mul_cancel
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
refine_4 :
  ∀ (x : ℕ),
    Eq (α := ℕ)
      ((toFinsuppAntidiag (n := d)
              {
                parts :=
                  (Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
                    { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
                      mem_support_toFun := ⋯ : ℕ →₀ ℕ },
                parts_pos := ⋯, parts_sum := ⋯ : d.Partition } :
            (a : ℕ) → ℕ)
          x :
        ℕ)
      ((g : (a : ℕ) → ℕ) x : ℕ)
⊢ toFinsuppAntidiag (n := d)
      {
        parts :=
          (Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ : ℕ →₀ ℕ },
        parts_pos := ⋯, parts_sum := ⋯ : d.Partition } =
    g

Tactic:
ext x
-- 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 : ℕ) (_ : 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)
hgne0 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i
x : ℕ
⊢ Eq (α := ℕ)
    ((toFinsuppAntidiag (n := d)
            {
              parts :=
                (Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
                  { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
                    mem_support_toFun := ⋯ : ℕ →₀ ℕ },
              parts_pos := ⋯, parts_sum := ⋯ : d.Partition } :
          (a : ℕ) → ℕ)
        x :
      ℕ)
    ((g : (a : ℕ) → ℕ) x : ℕ)

Tactic:
simpa [toFinsuppAntidiag] using Nat.div_mul_cancel <| aux_dvd_of_coeff_ne_zero hs0 hg hprod x

Premises used: _private.0.Nat.Partition.aux_dvd_of_coeff_ne_zero, Nat.div_mul_cancel, Nat.Partition.toFinsuppAntidiag
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
simp_rw :
  Eq.{u_1 + 1} (α := R) (∏ x ∈ p.parts.toFinset, f x (Multiset.count x p.parts))
    (∏ i ∈ s,
      (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))))
⊢ Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) p.parts) f =
    ∏ i ∈ s,
      (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))))

Tactic:
simp_rw [Finsupp.prod, Multiset.toFinsupp_support, Multiset.toFinsupp_apply]

Premises used: Multiset.toFinsupp_apply, Multiset.toFinsupp_support, Finsupp.prod
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
h : p.parts.toFinset ⊆ s
hg :
  ∀ x ∈ s \ p.parts.toFinset,
    Eq (α := R)
      ((coeff ((p.toFinsuppAntidiag : (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)
      (1 : R)
hfg :
  ∀ x ∈ p.parts.toFinset,
    f x (Multiset.count x p.parts) =
      (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) x) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f x (j + 1) • HPow.hPow (α := R⟦X⟧) X (x * (j + 1))))
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ p.parts.toFinset, f x (Multiset.count x p.parts))
    (∏ i ∈ s,
      (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
        (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))))

Tactic:
apply prod_subset_one_on_sdiff

Premises used: Finset.prod_subset_one_on_sdiff
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ p.parts.toFinset ⊆ s

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s \ p.parts.toFinset
⊢ x ∈ s ∧ x ∉ p.parts

Tactic:
rw [mem_sdiff, Multiset.mem_toFinset] at hx

Premises used: Finset.mem_sdiff, Multiset.mem_toFinset
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s ∧ x ∉ p.parts
⊢ x ≠ 0

Tactic:
have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx.1)
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s ∧ x ∉ p.parts
hx0 : x ≠ 0
⊢ Eq.{u_1 + 1} (α := R)
    ((constantCoeff : (a : R⟦X⟧) → R) (∑' (i : ℕ), f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)
    (∑' (i : ℕ), (constantCoeff : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)

Tactic:
have hsum := (summable_genFun_term' f hx0).map_tsum _
      (WithPiTopology.continuous_constantCoeff R)
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s ∧ x ∉ p.parts
hx0 : x ≠ 0
hsum :
  Eq.{u_1 + 1} (α := R)
    ((constantCoeff : (a : R⟦X⟧) → R) (∑' (i : ℕ), f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)
    (∑' (i : ℕ), (constantCoeff : (a : R⟦X⟧) → R) (f x (i + 1) • HPow.hPow (α := R⟦X⟧) X (x * (i + 1))) : R)
⊢ Eq (α := R)
    ((coeff ((p.toFinsuppAntidiag : (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)
    (1 : R)

Tactic:
simp [toFinsuppAntidiag, hsum, hx.2, hx0]

Premises used: And.right, Nat.Partition.toFinsuppAntidiag
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts.toFinset
⊢ i ∈ p.parts

Tactic:
rw [Multiset.mem_toFinset] at hi

Premises used: Multiset.mem_toFinset
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
⊢ i ≠ 0

Tactic:
have hi0 : i ≠ 0 := (p.parts_pos hi).ne.symm
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
hfg :
  f i (Multiset.count i p.parts) =
    HAdd.hAdd (α := R) (β := R) ((coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i_1 : ℕ),
          (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
            (f i (i_1 + 1) • HPow.hPow (α := R⟦X⟧) X (i * (i_1 + 1))) :
        R)
⊢ f i (Multiset.count i p.parts) =
    (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
      (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))))

Tactic:
rw [map_add, (summable_genFun_term' f hi0).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
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
this :
  f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0
⊢ f i (Multiset.count i p.parts) =
    HAdd.hAdd (α := R) (β := R) ((coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i_1 : ℕ),
          (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
            (f i (i_1 + 1) • HPow.hPow (α := R⟦X⟧) X (i * (i_1 + 1))) :
        R)

Tactic:
simpa [toFinsuppAntidiag, hi, hi0, coeff_X_pow]

Premises used: Nat.Partition.toFinsuppAntidiag, PowerSeries.coeff_X_pow
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
hfg : f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0
⊢ f i (Multiset.count i p.parts) =
    HAdd.hAdd (α := R) (β := R) ((coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R) 1 : R)
      (∑' (i_1 : ℕ),
          (coeff ((p.toFinsuppAntidiag : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
            (f i (i_1 + 1) • HPow.hPow (α := R⟦X⟧) X (i * (i_1 + 1))) :
        R)

Tactic:
suffices f i (Multiset.count i p.parts) =
        ∑' j, if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0 by
      simpa [toFinsuppAntidiag, hi, hi0, coeff_X_pow]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
hfg :
  f i (Multiset.count i p.parts) =
    if Multiset.count i p.parts * i = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0
rw :
  ∀ (b' : ℕ),
    b' ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b' + 1) then f i (b' + 1) else 0) = 0
⊢ f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0

Tactic:
rw [tsum_eq_single (Multiset.count i p.parts - 1) ?_]

Premises used: Nat.Partition.parts, HSub.hSub, Multiset.count, tsum_eq_single, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
hfg :
  f i (Multiset.count i p.parts) =
    if i * Multiset.count i p.parts = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0
⊢ f i (Multiset.count i p.parts) =
    if Multiset.count i p.parts * i = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
⊢ f i (Multiset.count i p.parts) =
    if i * Multiset.count i p.parts = i * (Multiset.count i p.parts - 1 + 1) then f i (Multiset.count i p.parts - 1 + 1)
    else 0

Tactic:
simp [Nat.sub_add_cancel (Multiset.one_le_count_iff_mem.mpr hi)]

Premises used: Iff.mpr, Nat.sub_add_cancel, Multiset.one_le_count_iff_mem
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
this : Multiset.count i p.parts * i ≠ i * (b + 1)
⊢ (if Multiset.count i p.parts * i = i * (b + 1) then f i (b + 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
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
suffices : Multiset.count i p.parts * i ≠ i * (b + 1)
⊢ (if Multiset.count i p.parts * i = i * (b + 1) then f i (b + 1) else 0) = 0

Tactic:
suffices Multiset.count i p.parts * i ≠ i * (b + 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
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
rw : Multiset.count i p.parts ≠ b + 1
⊢ Multiset.count i p.parts * i ≠ i * (b + 1)

Tactic:
rw [mul_comm i, (mul_left_inj' (Nat.ne_zero_of_lt (p.parts_pos hi))).ne]

Premises used: Iff.ne, mul_comm, Nat.Partition.parts_pos, Nat.ne_zero_of_lt, mul_left_inj'
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
hb : b ≠ Multiset.count i p.parts - 1
⊢ Multiset.count i p.parts ≠ b + 1

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
rw :
  ∀ (d : ℕ),
    Filter.Tendsto (β := R)
      (fun (i : Finset ℕ) ↦
        ((coeff d : (a : R⟦X⟧) → R)
            (∏ b ∈ i,
              HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (b + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((b + 1) * (j + 1)))) :
          R))
      (SummationFilter.unconditional ℕ).filter (nhds ((coeff d : (a : R⟦X⟧) → R) (genFun f)) : Filter R)
⊢ HasProd
    (fun (i : ℕ) ↦
      HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
    (genFun f)

Tactic:
rw [HasProd, WithPiTopology.tendsto_iff_coeff_tendsto]

Premises used: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto, HasProd, 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 : ℕ),
    Filter.Tendsto (β := R)
      (fun (i : Finset ℕ) ↦
        ((coeff d : (a : R⟦X⟧) → R)
            (∏ b ∈ i,
              HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (b + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((b + 1) * (j + 1)))) :
          R))
      (SummationFilter.unconditional ℕ).filter (nhds ((coeff d : (a : R⟦X⟧) → R) (genFun f)) : Filter R)

Tactic:
fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ range d) ↦ ?_)

Premises used: iInf, Filter.atTop, tendsto_atTop_of_eventually_const
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
refine :
  ∀ (d : ℕ) (s : Finset ℕ) (hs : s ≥ range d),
    Eq (α := R)
      ((coeff d : (a : R⟦X⟧) → R)
          (∏ b ∈ s,
            HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (b + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((b + 1) * (j + 1)))) :
        R)
      ((coeff d : (a : R⟦X⟧) → R) (genFun f) : R)
⊢ ∀ (d : ℕ),
    Filter.Tendsto (β := R)
      (fun (i : Finset ℕ) ↦
        ((coeff d : (a : R⟦X⟧) → R)
            (∏ b ∈ i,
              HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (b + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((b + 1) * (j + 1)))) :
          R))
      (SummationFilter.unconditional ℕ).filter (nhds ((coeff d : (a : R⟦X⟧) → R) (genFun f)) : Filter R)

Tactic:
refine fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ range d) ↦ ?_)

Premises used: tendsto_atTop_of_eventually_const
-- 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 ℕ
hs : s ≥ range d
⊢ Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏ i ∈ s, HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
    (∏ i ∈ Finset.map (addRightEmbedding 1) s,
      HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))))

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 ℕ
hs : s ≥ range d
⊢ Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏ i ∈ s, HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
    (∏ i ∈ Finset.map (addRightEmbedding 1) s,
      HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))))

Tactic:
have : ∏ i ∈ s, ((1 : R⟦X⟧) + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1)))
      = ∏ i ∈ s.map (addRightEmbedding 1), (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) := 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 ℕ
hs : s ≥ range d
this :
  Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏ i ∈ s, HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
    (∏ i ∈ Finset.map (addRightEmbedding 1) s,
      HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1))))
rw :
  Eq (α := R)
    ((coeff d : (a : R⟦X⟧) → R)
        (∏ i ∈ Finset.map (addRightEmbedding 1) s,
          HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))) :
      R)
    ((coeff d : (a : R⟦X⟧) → R) (genFun f) : R)
⊢ Eq (α := R)
    ((coeff d : (a : R⟦X⟧) → R)
        (∏ b ∈ s,
          HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (b + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((b + 1) * (j + 1)))) :
      R)
    ((coeff d : (a : R⟦X⟧) → R) (genFun f) : R)

Tactic:
rw [this]