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 ℕ
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)
        (∏ 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)
have hs₁ : 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
-- 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_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 (α := 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)
have 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)
Tactic: rw [coeff_genFun, coeff_prod]
-- 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_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)
have refine_1 : Set.MapsTo toFinsuppAntidiag (↑univ : Set d.Partition)
  (↑((Finset.map (addRightEmbedding 1) s).finsuppAntidiag d) : Set (ℕ →₀ ℕ))
Tactic: refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).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
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 (ℕ →₀ ℕ))
⊢ 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)
have 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
Tactic: refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).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
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
⊢ 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)
have 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))))
Tactic: refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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 : ℕ) ↦ if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n p)) : R))
have 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))))
Tactic: convert! hasProd_genFun (fun i c ↦ if p i then (1 : R) else 0) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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))))
⊢ 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))
have 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)
Tactic: convert! hasProd_genFun (fun i c ↦ if p i then (1 : R) else 0) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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
⊢ 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))))
have 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))))
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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 : ℕ
⊢ (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))))
have 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))))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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))))
⊢ (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))))
have neg : ¬p (i + 1) →
  1 = HAdd.hAdd (α := R⟦X⟧) 1 (∑' (j : ℕ), HSMul.hSMul (α := R) 0 (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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)
⊢ ∑' (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))))
have 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))))
Tactic: rw [tsum_eq_zero_add' ?_]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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))))
⊢ ∑' (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))))
have rw : Summable.{u_1, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ HPow.hPow (α := R⟦X⟧) X ((i + 1) * (n + 1))
Tactic: rw [tsum_eq_zero_add' ?_]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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.{u_1, 0} (α := R⟦X⟧) fun (n : ℕ) ↦ HPow.hPow (α := R⟦X⟧) X ((i + 1) * (n + 1))
have 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
Tactic: simp_rw [pow_mul, pow_add]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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.{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
have hf : Summable (HPow.hPow (HPow.hPow (α := R⟦X⟧) X i * HPow.hPow (α := R⟦X⟧) (β := ℕ) X 1))
Tactic: apply Summable.mul_right
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
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
⊢ 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)
have h : Eq.{u_1 + 1} (α := R⟦X⟧)
  (PowerSeries.mk fun (n : ℕ) ↦ (↑(∑ i : n.Partition, if ∀ i_1 ∈ i.parts, p i_1 then 1 else 0) : R))
  (PowerSeries.mk fun (n : ℕ) ↦
    ∑ x : n.Partition,
      if
          ∀ (i : ℕ),
            Membership.mem (γ := Finset ℕ)
                (Finsupp.support (M := ℕ) ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) x.parts)) i →
              p i then
        1
      else 0)
Tactic: simp_rw [genFun, restricted, card_filter, Finsupp.prod, prod_boole]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
⊢ HasProd.{u_1, 0} (α := R⟦X⟧) (fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have a : Nontrivial R
Tactic: nontriviality R using Subsingleton.eq_one
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
⊢ HasProd.{u_1, 0} (α := R⟦X⟧) (fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have h : Eq.{u_1 + 1} (α := ℕ → R⟦X⟧) (fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)) fun (i : ℕ) ↦
  HAdd.hAdd (α := R⟦X⟧) 1
    (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
Tactic: convert! hasProd_genFun (fun i c ↦ if c < m then (1 : R) else 0) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
h :
  Eq.{u_1 + 1} (α := ℕ → R⟦X⟧) (fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)) fun (i : ℕ) ↦
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
⊢ HasProd.{u_1, 0} (α := R⟦X⟧) (fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have h₁ : Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
  (genFun fun (i c : ℕ) ↦ if c < m then 1 else 0)
Tactic: convert! hasProd_genFun (fun i c ↦ if c < m then (1 : R) else 0) using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := ℕ → R⟦X⟧) (fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)) fun (i : ℕ) ↦
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
have h : ∀ (i : ℕ),
  ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) =
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
⊢ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) =
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
have h : HPow.hPow (α := R⟦X⟧) X ((i + 1) * 0) + ∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)) =
  HAdd.hAdd (α := R⟦X⟧) 1
    (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
Tactic: rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
⊢ HPow.hPow (α := R⟦X⟧) X ((i + 1) * 0) + ∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)) =
    HAdd.hAdd (α := R⟦X⟧) 1
      (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
have h : Eq.{u_1 + 1} (α := R⟦X⟧) (∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)))
  (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
Tactic: congrm $(by simp) + ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)))
    (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
have trans : Eq.{u_1 + 1} (α := R⟦X⟧) (∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)))
  (∑ k ∈ range (m - 1), HSMul.hSMul (α := R) (if k + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (k + 1))))
Tactic: trans ∑ k ∈ range (m - 1), (if k + 1 < m then (1 : R) else 0) • X ^ ((i + 1) * (k + 1))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
trans :
  Eq.{u_1 + 1} (α := R⟦X⟧) (∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)))
    (∑ k ∈ range (m - 1),
      HSMul.hSMul (α := R) (if k + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (k + 1))))
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)))
    (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
have trans₁ : Eq.{u_1 + 1} (α := R⟦X⟧)
  (∑ k ∈ range (m - 1), HSMul.hSMul (α := R) (if k + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (k + 1))))
  (∑' (j : ℕ), HSMul.hSMul (α := R) (if j + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (j + 1))))
Tactic: trans ∑ k ∈ range (m - 1), (if k + 1 < m then (1 : R) else 0) • X ^ ((i + 1) * (k + 1))
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∑ k ∈ range (m - 1), HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + k)))
    (∑ k ∈ range (m - 1),
      HSMul.hSMul (α := R) (if k + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (k + 1))))
have refine : ∀ (b : ℕ) (hn : b ∈ range (m - 1)),
  HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + b)) =
    HSMul.hSMul (α := R) (if b + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)))
Tactic: refine sum_congr rfl fun b hn ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
⊢ HPow.hPow (α := R⟦X⟧) X ((i + 1) * (1 + b)) =
    HSMul.hSMul (α := R) (if b + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)))
have rw : HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)) =
  HSMul.hSMul (α := R) (if b + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)))
Tactic: rw [add_comm 1 b]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (hypothesis)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
⊢ HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)) =
    HSMul.hSMul (α := R) (if b + 1 < m then 1 else 0) (HPow.hPow (α := R⟦X⟧) X ((i + 1) * (b + 1)))
have this : b + 1 < m
Tactic: have : b + 1 < m := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
    (genFun fun (i c : ℕ) ↦ if c < m then 1 else 0)
have h : Eq.{u_1 + 1} (α := R⟦X⟧)
  (PowerSeries.mk fun (n : ℕ) ↦
    (↑(∑ i : n.Partition, if ∀ i_1 ∈ i.parts, Multiset.count i_1 i.parts < m then 1 else 0) : R))
  (PowerSeries.mk fun (n : ℕ) ↦
    ∑ x : n.Partition,
      if
          ∀ (i : ℕ),
            Membership.mem (γ := Finset ℕ)
                (Finsupp.support (M := ℕ) ((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) x.parts)) i →
              (((Multiset.toFinsupp : (a : Multiset ℕ) → ℕ →₀ ℕ) x.parts : ℕ →₀ ℕ) : (a : ℕ) → ℕ) i < m then
        1
      else 0)
Tactic: simp_rw [genFun, countRestricted, card_filter, Finsupp.prod, prod_boole]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)
have inl : Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range 0, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)
Tactic: rcases Nat.eq_zero_or_pos m with rfl | hm
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
inl : Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range 0, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)
have inr : ∀ (hm : m > 0), Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)
Tactic: rcases Nat.eq_zero_or_pos m with rfl | hm