awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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⟧)
    (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)
⊢ 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:
simp_rw [genFun, restricted, card_filter, Finsupp.prod, prod_boole]

Premises used: Nat.Partition.restricted, Finset.card_filter, Finset.prod_boole, Nat.Partition.genFun, Finsupp.prod
-- 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
⊢ 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
-- 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
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦
    if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1

Tactic:
(hasProd_powerSeriesMk_card_restricted R p).multipliable

Premises used: Nat.Partition.hasProd_powerSeriesMk_card_restricted, HasProd.multipliable
-- 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
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n p)) : R))
    (∏' (i : ℕ), if p (i + 1) then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)

Tactic:
(hasProd_powerSeriesMk_card_restricted R p).tprod_eq.symm

Premises used: HasProd.tprod_eq, Nat.Partition.hasProd_powerSeriesMk_card_restricted, Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
⊢ Nontrivial R

Tactic:
nontriviality R using Subsingleton.eq_one

Premises used: Subsingleton.eq_one
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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 : ℕ) ↦
      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)))))
    (genFun fun (i c : ℕ) ↦ if c < m then 1 else 0)

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

Premises used: LT.lt, 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
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))))
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)
⊢ 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))

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

Premises used: LT.lt, 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
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
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))))
⊢ 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:
ext1 i
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
i : ℕ
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))))
⊢ ∑ 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:
rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range]

Premises used: Finset.sum_Ico_eq_sum_range, Finset.sum_range_eq_add_Ico
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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) = 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
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
i : ℕ
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))))
⊢ 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:
congrm $(by simp) + ?_
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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))))
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))))
⊢ 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:
trans ∑ k ∈ range (m - 1), (if k + 1 < m then (1 : R) else 0) • X ^ ((i + 1) * (k + 1))

Premises used: HSub.hSub, PowerSeries.X, Finset.range, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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))))

Tactic:
sum_congr rfl fun b hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
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)))
⊢ 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:
refine sum_congr rfl fun b hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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)
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)))
⊢ 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:
rw [add_comm 1 b]

Premises used: add_comm, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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)
⊢ b + 1 < m

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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)
⊢ b + 1 < m

Tactic:
have : b + 1 < m := by grind
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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)
this : b + 1 < m
⊢ 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:
simp [this]
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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 : ℕ
hb : b ∉ range (m - 1)
⊢ Eq.{u_1 + 1} (α := R) (if b + 1 < m then 1 else 0) 0

Tactic:
simpa using hb
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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),
      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:
exact (tsum_eq_sum (fun b hb ↦ smul_eq_zero_of_left (by simpa using hb) _)).symm

Premises used: smul_eq_zero_of_left, tsum_eq_sum, Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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⟧)
    (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)
⊢ 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:
simp_rw [genFun, countRestricted, card_filter, Finsupp.prod, prod_boole]

Premises used: Nat.Partition.countRestricted, Finset.card_filter, Finset.prod_boole, Nat.Partition.genFun, Finsupp.prod
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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 : ℕ) ↦
      (↑(∑ 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
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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)
inr :
  ∀ (hm : m > 0), Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range m, 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)

Tactic:
rcases Nat.eq_zero_or_pos m with rfl | hm

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range 0, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)

Tactic:
simpa using multipliable_of_exists_eq_zero ⟨0, rfl⟩

Premises used: multipliable_of_exists_eq_zero, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)

Tactic:
(hasProd_powerSeriesMk_card_countRestricted R hm).multipliable

Premises used: Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, HasProd.multipliable
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable.{u_1, 0} (α := R⟦X⟧) fun (i : ℕ) ↦ ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)

Tactic:
exact (hasProd_powerSeriesMk_card_countRestricted R hm).multipliable

Premises used: Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, HasProd.multipliable
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommSemiring R
m : ℕ
hm : 0 < m
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
    (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))

Tactic:
(hasProd_powerSeriesMk_card_countRestricted R hm).tprod_eq.symm

Premises used: Nat.Partition.hasProd_powerSeriesMk_card_countRestricted, HasProd.tprod_eq, Eq.symm
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
rw :
  Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏' (b : ℕ),
      (if ¬m ∣ b + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((b + 1) * j) else 1) *
        (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)))
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m)))
⊢ HMul.hMul (α := R⟦X⟧) (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
      (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))) =
    ∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m))

Tactic:
rw [← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
    (multipliable_one_sub_X_pow _)]

Premises used: Dvd.dvd, Nat.Partition.multipliable_powerSeriesMk_card_restricted, Multipliable.tprod_mul, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow, Not
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
simp_rw :
  Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏' (b : ℕ),
      if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
      else (∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X (b + 1) ^ j) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)))
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m))
⊢ Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏' (b : ℕ),
      (if ¬m ∣ b + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((b + 1) * j) else 1) *
        (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)))
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m)))

Tactic:
simp_rw [ite_not, ite_mul, pow_mul]

Premises used: pow_mul, ite_mul, ite_not
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
h :
  ∀ (b : ℕ),
    if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
    else (∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X (b + 1) ^ j) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
| fun (b : ℕ) ↦
    if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
    else (∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X (b + 1) ^ j) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))

Tactic:
ext b
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
b : ℕ
⊢ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) (HPow.hPow (α := R⟦X⟧) X (b + 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
b : ℕ
h : if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1
| if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
  else (∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X (b + 1) ^ j) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))

Tactic:
rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]

Premises used: PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
h : ∀ (b : ℕ), if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1
| fun (b : ℕ) ↦
    if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
    else (∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X (b + 1) ^ j) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))

Tactic:
ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]

Premises used: PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
conv :
  Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (b : ℕ), if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1)
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m))
⊢ Eq.{u_1 + 1} (α := R⟦X⟧)
    (∏' (b : ℕ),
      if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1))
      else (∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X (b + 1) ^ j) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)))
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m))

Tactic:
conv in fun b ↦ _ =>
    ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]

Premises used: PowerSeries.WithPiTopology.tsum_pow_mul_one_sub_of_constantCoeff_eq_zero
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (b : ℕ), if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1)
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m))

Tactic:
tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 1) ?_ ?_ ?_

Premises used: HMul.hMul, HSub.hSub, tprod_eq_tprod_of_ne_one_bij, HAdd.hAdd, OfNat.ofNat, Subtype.val
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : T2Space R
inst_2 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
refine_1 :
  Function.Injective (β := ℕ)
    fun
      (i : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)) ↦
    ((↑i : ℕ) + 1) * m - 1
refine_2 :
  Subset (α := Set ℕ)
    (Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (b : ℕ) ↦
      if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1)
    (Set.range
      fun
        (i :
          (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)) ↦
      ((↑i : ℕ) + 1) * m - 1)
refine_3 :
  ∀ (x : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)),
    (if
          m ∣
            HAdd.hAdd (α := ℕ)
              ((fun
                    (i :
                      (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦
                            1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) :
                        Type)) ↦
                  ((↑i : ℕ) + 1) * m - 1)
                x)
              1 then
        1 *
          (1 -
            HPow.hPow (α := R⟦X⟧) X
              (HAdd.hAdd (α := ℕ)
                ((fun
                      (i :
                        (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦
                              1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) :
                          Type)) ↦
                    ((↑i : ℕ) + 1) * m - 1)
                  x)
                1))
      else 1) =
      1 - HPow.hPow (α := R⟦X⟧) X ((↑x : ℕ) + 1) ^ m
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (b : ℕ), if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1)
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m))

Tactic:
refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 1) ?_ ?_ ?_

Premises used: HMul.hMul, HSub.hSub, tprod_eq_tprod_of_ne_one_bij, HAdd.hAdd, OfNat.ofNat, Subtype.val