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 ℕ
hs : s ≥ range d
this_1 :
  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 : ℕ
this : 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i
⊢ i ∈ Icc 1 d → i ∈ Finset.map (addRightEmbedding 1) s

Tactic:
simpa
-- 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))))
i : ℕ
suffices : 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i
⊢ i ∈ Icc 1 d → i ∈ Finset.map (addRightEmbedding 1) s

Tactic:
suffices 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i by simpa
-- 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))))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ ∃ a ∈ s, a + 1 = i

Tactic:
⟨i - 1, mem_of_subset hs ?_, ?_⟩

Premises used: HSub.hSub, And.intro, Exists.intro, OfNat.ofNat, 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 ℕ
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
refine_2 : i - 1 + 1 = i
⊢ ∃ a ∈ s, a + 1 = i

Tactic:
refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩
-- 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))))
i : ℕ
h1 : 1 ≤ i
h2 : i ≤ d
⊢ i - 1 ∈ range d

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 ℕ
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
⊢ i - 1 + 1 = i

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 ℕ
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))))
⊢ Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s

Tactic:
have hs : Icc 1 d ⊆ s.map (addRightEmbedding 1) := by
    intro i
    suffices 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i by simpa
    intro h1 h2
    refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩ <;> 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 ℕ
hs_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ l ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
      ∏ i ∈ Finset.map (addRightEmbedding 1) s,
        (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))))
    (∑ p : d.Partition, Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) p.parts) f)
⊢ 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 [coeff_genFun, coeff_prod]

Premises used: PowerSeries.coeff_prod, Nat.Partition.coeff_genFun
-- 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_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ Eq.{u_1 + 1} (α := R)
    (∑ l ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
      ∏ i ∈ Finset.map (addRightEmbedding 1) s,
        (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))))
    (∑ p : d.Partition, Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) p.parts) f)

Tactic:
(sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm

Premises used: Function.Injective.injOn, Finset.sum_of_injOn, Nat.Partition.toFinsuppAntidiag_injective, Nat.Partition.toFinsuppAntidiag, Eq.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
d : ℕ
s : Finset ℕ
hs_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
refine_1 :
  Set.MapsTo toFinsuppAntidiag (↑univ : Set d.Partition)
    (↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) : Set (ℕ →₀ ℕ))
refine_2 :
  ∀ (i : ℕ →₀ ℕ),
    Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) i →
      i ∉ toFinsuppAntidiag '' (↑univ : Set d.Partition) →
        Eq.{u_1 + 1} (α := R)
          (∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
            (coeff ((i : (a : ℕ) → ℕ) i_1) : (a : R⟦X⟧) → R)
              (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i_1 (j + 1) • HPow.hPow (α := R⟦X⟧) X (i_1 * (j + 1)))))
          0
refine_3 :
  ∀ (i : d.Partition),
    Membership.mem (γ := Finset d.Partition) univ i →
      Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) i.parts) f =
        ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
          (coeff ((i.toFinsuppAntidiag : (a : ℕ) → ℕ) i_1) : (a : R⟦X⟧) → R)
            (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i_1 (j + 1) • HPow.hPow (α := R⟦X⟧) X (i_1 * (j + 1))))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ l ∈ (Finset.map (addRightEmbedding 1) s).finsuppAntidiag d,
      ∏ i ∈ Finset.map (addRightEmbedding 1) s,
        (coeff ((l : (a : ℕ) → ℕ) i) : (a : R⟦X⟧) → R)
          (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i (j + 1) • HPow.hPow (α := R⟦X⟧) X (i * (j + 1)))))
    (∑ p : d.Partition, Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) p.parts) f)

Tactic:
refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm

Premises used: Function.Injective.injOn, Finset.sum_of_injOn, Nat.Partition.toFinsuppAntidiag_injective, Nat.Partition.toFinsuppAntidiag, Eq.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
d : ℕ
s : Finset ℕ
hs_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
p : d.Partition
refine_1 :
  p ∈ (↑univ : Set d.Partition) →
    p.toFinsuppAntidiag ∈ (↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) : Set (ℕ →₀ ℕ))
⊢ p ∈ (↑univ : Set d.Partition) →
    p.toFinsuppAntidiag ∈ (↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) : Set (ℕ →₀ ℕ))

Tactic:
_
-- 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_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
p : d.Partition
h : p ∈ (↑univ : Set d.Partition)
⊢ p.toFinsuppAntidiag ∈ (↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) : Set (ℕ →₀ ℕ))

Tactic:
mem_of_subset (finsuppAntidiag_mono hs.le _) p.toFinsuppAntidiag_mem_finsuppAntidiag

Premises used: Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag, HasSubset.Subset.le, Finset.finsuppAntidiag_mono, 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 ℕ
hs_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
p : d.Partition
h : p ∈ (↑univ : Set d.Partition)
⊢ p.toFinsuppAntidiag ∈ (↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) : Set (ℕ →₀ ℕ))

Tactic:
exact mem_of_subset (finsuppAntidiag_mono hs.le _) p.toFinsuppAntidiag_mem_finsuppAntidiag

Premises used: Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag, HasSubset.Subset.le, Finset.finsuppAntidiag_mono, 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 ℕ
hs_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) g
hg' : g ∉ toFinsuppAntidiag '' (↑univ : Set d.Partition)
⊢ 0 ∉ Finset.map (addRightEmbedding 1) s

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_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
g : ℕ →₀ ℕ
hg : Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) g
hg' : g ∉ toFinsuppAntidiag '' (↑univ : Set d.Partition)
⊢ g ∉ Set.range (ι := d.Partition) toFinsuppAntidiag

Tactic:
simpa using hg'
-- 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_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∀ (i : ℕ →₀ ℕ),
    Membership.mem (γ := Finset (ℕ →₀ ℕ)) ((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) i →
      i ∉ toFinsuppAntidiag '' (↑univ : Set d.Partition) →
        Eq.{u_1 + 1} (α := R)
          (∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
            (coeff ((i : (a : ℕ) → ℕ) i_1) : (a : R⟦X⟧) → R)
              (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i_1 (j + 1) • HPow.hPow (α := R⟦X⟧) X (i_1 * (j + 1)))))
          0

Tactic:
exact fun g hg hg' ↦ aux_prod_coeff_eq_zero_of_notMem_range f (by simp) hg (by simpa using hg')

Premises used: _private.0.Nat.Partition.aux_prod_coeff_eq_zero_of_notMem_range
-- 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_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
p : d.Partition
h : Membership.mem (γ := Finset d.Partition) univ p
⊢ 0 ∉ Finset.map (addRightEmbedding 1) s

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_1 : 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))))
hs : Icc 1 d ⊆ Finset.map (addRightEmbedding 1) s
⊢ ∀ (i : d.Partition),
    Membership.mem (γ := Finset d.Partition) univ i →
      Finsupp.prod ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) i.parts) f =
        ∏ i_1 ∈ Finset.map (addRightEmbedding 1) s,
          (coeff ((i.toFinsuppAntidiag : (a : ℕ) → ℕ) i_1) : (a : R⟦X⟧) → R)
            (HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f i_1 (j + 1) • HPow.hPow (α := R⟦X⟧) X (i_1 * (j + 1))))

Tactic:
exact fun p _ ↦ aux_prod_f_eq_prod_coeff f p hs.le (by simp)

Premises used: HasSubset.Subset.le, _private.0.Nat.Partition.aux_prod_f_eq_prod_coeff
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦
    HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1)))

Tactic:
(hasProd_genFun f).multipliable

Premises used: HasProd.multipliable, Nat.Partition.hasProd_genFun
-- Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : T2Space R
f : ℕ → ℕ → R
⊢ genFun f =
    ∏' (i : ℕ), HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), f (i + 1) (j + 1) • HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1)))

Tactic:
(hasProd_genFun f).tprod_eq.symm

Premises used: HasProd.tprod_eq, Nat.Partition.hasProd_genFun, Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
⊢ HasProd.{u_1, 0} (α := R⟦X⟧)
    (fun (i : ℕ) ↦
      HAdd.hAdd (α := R⟦X⟧) 1
        (∑' (j : ℕ), HSMul.hSMul (α := R) (if p (i + 1) then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1)))))
    (genFun fun (i c : ℕ) ↦ if p i then 1 else 0)

Tactic:
hasProd_genFun (fun i c ↦ if p i then (1 : R) else 0)

Premises used: Nat.Partition.hasProd_genFun, OfNat.ofNat, ite
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
h :
  Eq.{u_1 + 1} (α := ℕ → R⟦X⟧)
    (fun (i : ℕ) ↦ if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1) fun (i : ℕ) ↦
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if p (i + 1) then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
h₁ :
  Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n p)) : R))
    (genFun fun (i c : ℕ) ↦ if p i then 1 else 0)
⊢ HasProd.{u_1, 0} (α := R⟦X⟧)
    (fun (i : ℕ) ↦ if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n p)) : R))

Tactic:
convert! hasProd_genFun (fun i c ↦ if p i then (1 : R) else 0) using 1

Premises used: Nat.Partition.hasProd_genFun, OfNat.ofNat, ite
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
h :
  ∀ (i : ℕ),
    (if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1) =
      HAdd.hAdd (α := R⟦X⟧) 1
        (∑' (j : ℕ), HSMul.hSMul (α := R) (if p (i + 1) then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
⊢ Eq.{u_1 + 1} (α := ℕ → R⟦X⟧)
    (fun (i : ℕ) ↦ if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1) fun (i : ℕ) ↦
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if p (i + 1) then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))

Tactic:
ext1 i
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
pos :
  p (i + 1) →
    ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) =
      HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 1 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
neg :
  ¬p (i + 1) →
    1 = HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 0 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
⊢ (if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1) =
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if p (i + 1) then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))

Tactic:
split_ifs
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : p (i + 1)
pos :
  HPow.hPow (α := R⟦X⟧) X ((i + 1) * 0) + ∑' (b : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)) =
    HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 1 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
rw : Summable.{u_1, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ HPow.hPow (α := R⟦X⟧) X ((i + 1) * (n + 1))
⊢ ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) =
    HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 1 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))

Tactic:
rw [tsum_eq_zero_add' ?_]

Premises used: tsum_eq_zero_add'
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : p (i + 1)
⊢ HPow.hPow (α := R⟦X⟧) X ((i + 1) * 0) + ∑' (b : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)) =
    HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 1 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : p (i + 1)
simp_rw :
  Summable.{u_1, 0} (α := R⟦X⟧) fun (n : ℕ) ↦
    (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1) ^ n *
      HPow.hPow (β := ℕ) (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1) 1
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ HPow.hPow (α := R⟦X⟧) X ((i + 1) * (n + 1))

Tactic:
simp_rw [pow_mul, pow_add]

Premises used: pow_add, pow_mul
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : p (i + 1)
hf : Summable (HPow.hPow (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1))
⊢ Summable.{u_1, 0} (α := R⟦X⟧) fun (n : ℕ) ↦
    (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1) ^ n *
      HPow.hPow (β := ℕ) (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1) 1

Tactic:
apply Summable.mul_right

Premises used: Summable.mul_right
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : p (i + 1)
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1) : R)
    (0 : R)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : p (i + 1)
⊢ Summable (HPow.hPow (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1))

Tactic:
exact summable_pow_of_constantCoeff_eq_zero (by simp)

Premises used: PowerSeries.WithPiTopology.summable_pow_of_constantCoeff_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
inst_3 : IsTopologicalSemiring R
p : ℕ → Prop
inst_4 : DecidablePred p
i : ℕ
h : ¬p (i + 1)
⊢ 1 = HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 0 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))

Tactic:
simp