awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
⊢ Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }) =
    d
have h1 : s.sum (⇑g : (a : ℕ) → ℕ) = d
Tactic: obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
⊢ Multiset.sum
      ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
        { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
          mem_support_toFun := ⋯ }) =
    d
have h2 : g.support ⊆ s
Tactic: obtain ⟨h1, h2⟩ := mem_finsuppAntidiag.mp hg
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
have refine_3 : Eq (α := ℕ)
  (Multiset.sum
    ((Finsupp.toMultiset : (a : ℕ →₀ ℕ) → Multiset ℕ)
      { support := g.support, toFun := fun (i : ℕ) ↦ HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) i : ℕ) i,
        mem_support_toFun := sorry }))
  (s.sum (⇑g : (a : ℕ) → ℕ))
Tactic: refine Eq.trans ?_ h1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ 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 : ℕ) → ℕ))
have refine_3 : Eq (α := ℕ) (∑ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x) (∑ x ∈ s, (g : (a : ℕ) → ℕ) x)
Tactic: suffices ∑ x ∈ g.support, g x / x * x = ∑ x ∈ s, g x by simpa [Finsupp.sum]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ Eq (α := ℕ) (∑ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x) (∑ x ∈ s, (g : (a : ℕ) → ℕ) x)
have refine_3 : ∀ x ∈ g.support, HDiv.hDiv (α := ℕ) ((g : (a : ℕ) → ℕ) x : ℕ) x * x = (g : (a : ℕ) → ℕ) x
Tactic: apply sum_subset_zero_on_sdiff h2 (by simp)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ 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
have 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 := sorry : ℕ →₀ ℕ },
              parts_pos := sorry, parts_sum := sorry : d.Partition } :
          (a : ℕ) → ℕ)
        x :
      ℕ)
    ((g : (a : ℕ) → ℕ) x : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ 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))))
have 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)))))
Tactic: simp_rw [Finsupp.prod, Multiset.toFinsupp_support, Multiset.toFinsupp_apply]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ 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)))))
have h : p.parts.toFinset ⊆ s
Tactic: apply prod_subset_one_on_sdiff
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ 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)))))
have 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)
Tactic: apply prod_subset_one_on_sdiff
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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)
⊢ 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)))))
have 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))))
Tactic: apply prod_subset_one_on_sdiff
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
⊢ 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)
have hx₁ : x ∈ s ∧ x ∉ p.parts
Tactic: rw [mem_sdiff, Multiset.mem_toFinset] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
⊢ 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)
have hx0 : x ≠ 0
Tactic: have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx.1)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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 (α := 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)
have 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)
Tactic: have hsum := (summable_genFun_term' f hx0).map_tsum _
      (WithPiTopology.continuous_constantCoeff R)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
⊢ 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))))
have hi₁ : i ∈ p.parts
Tactic: rw [Multiset.mem_toFinset] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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
⊢ 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))))
have hi0 : i ≠ 0
Tactic: have hi0 : i ≠ 0 := (p.parts_pos hi).ne.symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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) =
    (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))))
have 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)
Tactic: rw [map_add, (summable_genFun_term' f hi0).map_tsum _ (WithPiTopology.continuous_coeff _ _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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) =
    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)
have 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
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]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0
have 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
Tactic: rw [tsum_eq_single (Multiset.count i p.parts - 1) ?_]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ 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
have 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
Tactic: rw [tsum_eq_single (Multiset.count i p.parts - 1) ?_]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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 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
have 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
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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
⊢ (if Multiset.count i p.parts * i = i * (b + 1) then f i (b + 1) else 0) = 0
have suffices : Multiset.count i p.parts * i ≠ i * (b + 1)
Tactic: suffices Multiset.count i p.parts * i ≠ i * (b + 1) by simp [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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 * i ≠ i * (b + 1)
have rw : Multiset.count i p.parts ≠ b + 1
Tactic: rw [mul_comm i, (mul_left_inj' (Nat.ne_zero_of_lt (p.parts_pos hi))).ne]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → 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)
have 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)
Tactic: rw [HasProd, WithPiTopology.tendsto_iff_coeff_tendsto]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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)
have 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)
Tactic: refine fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ range d) ↦ ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (hypothesis)
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 (α := 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)
have 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))))
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
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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))))
⊢ 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)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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))))
i : ℕ
⊢ i ∈ Icc 1 d → i ∈ Finset.map (addRightEmbedding 1) s
have suffices : 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i
Tactic: suffices 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i by simpa
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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))))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ ∃ a ∈ s, a + 1 = i
have refine_1 : i - 1 ∈ range d
Tactic: refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.GenFun (goal)
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))))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
refine_1 : i - 1 ∈ range d
⊢ ∃ a ∈ s, a + 1 = i
have refine_2 : i - 1 + 1 = i
Tactic: refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩