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 ∈ 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 : ∀ (hx : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)), x ∈ s
⊢ Eq (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
contrapose! 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
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 : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∈ g.support

Tactic:
simpa using 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
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 : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) (0 : ℕ)
⊢ x ∈ s

Tactic:
exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 <| by simpa using hx

Premises used: Finset.mem_finsuppAntidiag, And.right, Iff.mp, Finset.mem_of_subset
-- 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
this :
  ∃ i ∈ s,
    Eq (α := 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)
obtain :
  ∀ (i : ℕ) (hi : i ∈ s)
    (hi' :
      Eq (α := 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)),
    Eq.{u_1 + 1} (α := R)
      (∏ i ∈ s,
        (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)))))
      0
⊢ Eq.{u_1 + 1} (α := R)
    (∏ i ∈ s,
      (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)))))
    0

Tactic:
obtain ⟨i, hi, hi'⟩ := 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
i : ℕ
hi : i ∈ s
hi' :
  Eq (α := 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)
⊢ Eq.{u_1 + 1} (α := R)
    (∏ i ∈ s,
      (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)))))
    0

Tactic:
apply prod_eq_zero hi hi'

Premises used: Finset.prod_eq_zero
-- 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
suffices :
  ∃ i ∈ s,
    Eq (α := 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)
⊢ Eq.{u_1 + 1} (α := R)
    (∏ i ∈ s,
      (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)))))
    0

Tactic:
suffices ∃ i ∈ s, (coeff (g i)) ((1 : R⟦X⟧) + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) = 0 by
    obtain ⟨i, hi, hi'⟩ := this
    apply prod_eq_zero hi hi'
-- 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
hg' : g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag
contrapose! :
  ∀
    (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)),
    g ∈ Set.range (ι := d.Partition) toFinsuppAntidiag
⊢ ∃ i ∈ s,
    Eq (α := 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)

Tactic:
contrapose! hg' with 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 : ℕ) (_ : 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)
i : ℕ
⊢ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i → Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)

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
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)
i : ℕ
refine_1 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)), i ≠ 0
refine_2 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)), i ≤ (g : (a : ℕ) → ℕ) i
⊢ Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, by 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
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)
i : ℕ
h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)
refine_1 : ∀ (h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)), 0 ∈ s
⊢ i ≠ 0

Tactic:
contrapose hs0 with rfl

Premises used: rfl
-- 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 ℕ
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)
h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
⊢ 0 ∈ g.support

Tactic:
simpa using h
-- 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 ℕ
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)
h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) (0 : ℕ)
⊢ 0 ∈ s

Tactic:
exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h)

Premises used: Finset.mem_finsuppAntidiag, And.right, Iff.mp, Finset.mem_of_subset
-- 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)
i : ℕ
h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)
⊢ i ≤ (g : (a : ℕ) → ℕ) i

Tactic:
Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _

Premises used: _private.0.Nat.Partition.aux_dvd_of_coeff_ne_zero, Nat.pos_of_ne_zero, Nat.le_of_dvd
-- 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)
i : ℕ
h : Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ)
⊢ i ≤ (g : (a : ℕ) → ℕ) i

Tactic:
exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg hprod _

Premises used: _private.0.Nat.Partition.aux_dvd_of_coeff_ne_zero, Nat.pos_of_ne_zero, Nat.le_of_dvd
-- 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)
⊢ ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) ↔ i ≠ 0 ∧ i ≤ (g : (a : ℕ) → ℕ) i

Tactic:
have hgne0 (i : ℕ) : g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i := by
    refine ⟨fun h ↦ ⟨?_, ?_⟩, by grind⟩
    · contrapose hs0 with rfl
      exact mem_of_subset (mem_finsuppAntidiag.mp hg).2 (by simpa using h)
    · exact Nat.le_of_dvd (Nat.pos_of_ne_zero h) <| aux_dvd_of_coeff_ne_zero hs0 hg 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 : ℕ) (_ : 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
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g

Tactic:
⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩

Premises used: Finsupp.toMultiset, Nat.Partition.mk, Finsupp.support, Finsupp.mk, HDiv.hDiv, Exists.intro, DFunLike.coe
-- 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_1 : ∀ (a : ℕ), a ∈ g.support ↔ Ne (α := ℕ) ((fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i) a) 0
refine_2 :
  ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ)
        ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ } :
          Multiset ℕ)
        i →
      0 < i
refine_3 :
  Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }) =
    d
refine_4 :
  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
⊢ ∃ (y : d.Partition), y.toFinsuppAntidiag = g

Tactic:
refine ⟨Nat.Partition.mk (Finsupp.mk g.support (fun i ↦ g i / i) ?_).toMultiset ?_ ?_, ?_⟩
-- 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
⊢ ∀ (a : ℕ), a ∈ g.support ↔ Ne (α := ℕ) ((fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i) a) 0

Tactic:
simpa using hgne0
-- 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
this : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) → i ≠ 0
⊢ ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ)
        ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ } :
          Multiset ℕ)
        i →
      0 < i

Tactic:
simpa [Nat.pos_iff_ne_zero]

Premises used: Nat.pos_iff_ne_zero
-- 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_2 : ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) → i ≠ 0
⊢ ∀ {i : ℕ},
    Membership.mem (γ := Multiset ℕ)
        ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
            { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
              mem_support_toFun := ⋯ } :
          Multiset ℕ)
        i →
      0 < i

Tactic:
suffices ∀ i, g i ≠ 0 → i ≠ 0 by simpa [Nat.pos_iff_ne_zero]
-- 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
⊢ ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) → i ≠ 0

Tactic:
fun i h ↦ ((hgne0 i).mp h).1

Premises used: And.left, Iff.mp
-- 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
⊢ ∀ (i : ℕ), Ne (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) (0 : ℕ) → i ≠ 0

Tactic:
exact fun i h ↦ ((hgne0 i).mp h).1

Premises used: And.left, Iff.mp
-- 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
⊢ s.sum (⇑g : (a : ℕ) → ℕ) = d

Tactic:
obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg

Premises used: Finset.mem_finsuppAntidiag, Iff.mp
-- 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
⊢ g.support ⊆ s

Tactic:
obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg

Premises used: Finset.mem_finsuppAntidiag, Iff.mp
-- 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
⊢ Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }) =
    d

Tactic:
Eq.trans ?_ h1

Premises used: Eq.trans
-- 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 (α := ℕ)
    (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 : ℕ) → ℕ))
⊢ Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }) =
    d

Tactic:
refine Eq.trans ?_ h1

Premises used: Eq.trans
-- 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
this : 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:
simpa [Finsupp.sum]

Premises used: Finsupp.sum