awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < 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))
have a : Nontrivial R
Tactic: nontriviality R
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
⊢ 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))
have 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)))
Tactic: rw [← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
    (multipliable_one_sub_X_pow _)]
-- 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 : 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 ∑' (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)))
have 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))
Tactic: simp_rw [ite_not, ite_mul, pow_mul]
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
| 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))
have 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))
Tactic: ext b
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
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))
have h : if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1
Tactic: rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
| 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))
have h : ∀ (b : ℕ), if m ∣ b + 1 then 1 * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)) else 1
Tactic: ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (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 : 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 (∑' (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))
have 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))
Tactic: conv in fun b ↦ _ =>
    ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (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 : 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))
have 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
Tactic: refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 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 : 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
⊢ 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))
have 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)
Tactic: refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 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 : 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)
⊢ 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))
have 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
Tactic: refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
a b : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)
h :
  Eq (α := ℕ)
    ((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)
      a)
    ((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)
      b)
⊢ 1 ≤ ((↑a : ℕ) + 1) * m
have nlinarith : ((↑a : ℕ) + 1) * m < 1 →
  -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑m : ℤ)) + (HAdd.hAdd (α := ℤ) (↑(↑a : ℕ) : ℤ) 1 * (↑m : ℤ) + 1 - 1) +
      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) 0 (↑(↑a : ℕ) : ℤ)) =
    0
Tactic: nlinarith
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
a b : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)
h :
  Eq (α := ℕ)
    ((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)
      a)
    ((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)
      b)
⊢ 1 ≤ ((↑b : ℕ) + 1) * m
have nlinarith : ((↑b : ℕ) + 1) * m < 1 →
  -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑m : ℤ)) + (HAdd.hAdd (α := ℤ) (↑(↑b : ℕ) : ℤ) 1 * (↑m : ℤ) + 1 - 1) +
      (0 - HSub.hSub (α := ℤ) 0 (↑m : ℤ) * HSub.hSub (α := ℤ) 0 (↑(↑b : ℕ) : ℤ)) =
    0
Tactic: nlinarith
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h_1 : Nontrivial R
a b : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)
h :
  Eq (α := ℕ)
    ((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)
      a)
    ((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)
      b)
⊢ a = b
have h₁ : (↑a : ℕ) = (↑b : ℕ)
Tactic: rw [tsub_left_inj (by nlinarith) (by nlinarith), mul_left_inj' (hm.ne.symm), add_left_inj] at h
Cleared hypotheses: h
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
⊢ 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)
have refine_2 : ∀ (i : ℕ), m ∣ i + 1 → ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
Tactic: suffices ∀ (i : ℕ), m ∣ i + 1 → ∃ j ≠ 0, j * m - 1 = i by simpa
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
hi : m ∣ i + 1
⊢ ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
have refine_2 : ∀ (j : ℕ) (hj : i + 1 = m * j), ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
Tactic: obtain ⟨j, hj⟩ := dvd_def.mp hi
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
have refine_2 : j * m = i + 1
Tactic: refine ⟨j, by grind, Nat.sub_eq_of_eq_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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ j * m = i + 1
have refine_2 : j * m = m * j
Tactic: rw [hj, mul_comm m j]
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
refine_2 : j * m = m * j
⊢ j * m = i + 1
have refine_2₁ : j * m = j * m
Tactic: rw [hj, mul_comm m j]
-- 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 : CommRing R
inst_3 : NoZeroDivisors R
inst_4 : IsTopologicalRing R
m : ℕ
hm : 0 < m
h : Nontrivial R
i : (↑(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)
              i)
            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)
                i)
              1))
    else 1) =
    1 - HPow.hPow (α := R⟦X⟧) X ((↑i : ℕ) + 1) ^ m
have this : ((↑i : ℕ) + 1) * m - 1 + 1 = ((↑i : ℕ) + 1) * m
Tactic: have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n fun (x : ℕ) ↦ ¬m ∣ x)) : R))
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n fun (x : ℕ) ↦ ¬m ∣ x)) : R))
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have x : DiscreteTopology R
Tactic: have _ : DiscreteTopology R := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
h_1 : DiscreteTopology R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(restricted n fun (x : ℕ) ↦ ¬m ∣ x)) : R))
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have rw : Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
  (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
Tactic: rw [powerSeriesMk_card_restricted_eq_tprod R (¬ m ∣ ·)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
h_1 : DiscreteTopology R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
    (PowerSeries.mk fun (n : ℕ) ↦ (↑(#(countRestricted n m)) : R))
have rw : Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
  (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
Tactic: rw [powerSeriesMk_card_countRestricted_eq_tprod R hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
h_1 : DiscreteTopology R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), HPow.hPow (α := R⟦X⟧) X ((i + 1) * j) else 1)
    (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
have apply : 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))) =
  HMul.hMul (α := R⟦X⟧) (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1)))
Tactic: apply mul_right_cancel₀ (tprod_one_sub_X_pow_ne_zero R)
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
h_1 : DiscreteTopology R
⊢ 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))) =
    HMul.hMul (α := R⟦X⟧) (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
      (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1)))
have rw : ∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m)) =
  HMul.hMul (α := R⟦X⟧) (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
    (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1)))
Tactic: rw [aux_mul_one_sub_X_pow R hm]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
h_1 : DiscreteTopology R
⊢ ∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m)) =
    HMul.hMul (α := R⟦X⟧) (∏' (i : ℕ), ∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j))
      (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X (i + 1)))
have rw : Eq.{u_1 + 1} (α := R⟦X⟧) (∏' (i : ℕ), (1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m)))
  (∏' (b : ℕ), (∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((b + 1) * j)) * (1 - HPow.hPow (α := R⟦X⟧) X (b + 1)))
Tactic: rw [← (multipliable_powerSeriesMk_card_countRestricted R m).tprod_mul
    (multipliable_one_sub_X_pow _)]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
h_1 : DiscreteTopology R
i : ℕ
⊢ 1 - HPow.hPow (α := R⟦X⟧) X ((i + 1) * m) =
    (∑ j ∈ range m, HPow.hPow (α := R⟦X⟧) X ((i + 1) * j)) * (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))
have simp_rw : 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m =
  (∑ x ∈ range m, HPow.hPow (α := R⟦X⟧) X (i + 1) ^ x) * (1 - HPow.hPow (α := R⟦X⟧) X (i + 1))
Tactic: simp_rw [pow_mul, geom_sum_mul_neg]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Partition.Glaisher (goal)
Goal:
n : ℕ
⊢ #(odds n) = #(distincts n)
have simp_rw : #(restricted n fun (x : ℕ) ↦ ¬2 ∣ x) = #(countRestricted n 2)
Tactic: simp_rw [← countRestricted_two, odds, even_iff_two_dvd]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
k : ℤ
⊢ (↑(pentagonal k) : ℤ) = k * (3 * k - 1) / 2
have ofNat : (↑(pentagonal (Int.ofNat 0)) : ℤ) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2
Tactic: rcases k with (_ | _) | _
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
k : ℤ
ofNat : (↑(pentagonal (Int.ofNat 0)) : ℤ) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2
⊢ (↑(pentagonal k) : ℤ) = k * (3 * k - 1) / 2
have ofNat₁ : ∀ (n : ℕ), (↑(pentagonal (Int.ofNat (n + 1))) : ℤ) = Int.ofNat (n + 1) * (3 * Int.ofNat (n + 1) - 1) / 2
Tactic: rcases k with (_ | _) | _
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
k : ℤ
ofNat : (↑(pentagonal (Int.ofNat 0)) : ℤ) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2
ofNat₁ : ∀ (n : ℕ), (↑(pentagonal (Int.ofNat (n + 1))) : ℤ) = Int.ofNat (n + 1) * (3 * Int.ofNat (n + 1) - 1) / 2
⊢ (↑(pentagonal k) : ℤ) = k * (3 * k - 1) / 2
have negSucc : ∀ (a : ℕ), (↑(pentagonal (Int.negSucc a)) : ℤ) = Int.negSucc a * (3 * Int.negSucc a - 1) / 2
Tactic: rcases k with (_ | _) | _
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
k : ℤ
⊢ HMul.hMul (α := ℤ) 2 (↑(pentagonal k) : ℤ) = k * (3 * k - 1)
have rw : 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1)
Tactic: rw [natCast_pentagonal]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (hypothesis)
Goal:
x y : ℤ
h : pentagonal x = pentagonal y
⊢ x = y
have h₁ : (3 * (x + y) - 1) * (x - y) = 0
Tactic: replace h : (3 * (x + y) - 1) * (x - y) = 0 := by grind [two_mul_natCast_pentagonal]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
⊢ x = y
have inl : 3 * (x + y) - 1 = 0 → x = y
Tactic: cases mul_eq_zero.mp h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
inl : 3 * (x + y) - 1 = 0 → x = y
⊢ x = y
have inr : x - y = 0 → x = y
Tactic: cases mul_eq_zero.mp h
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
⊢ StrictMonoOn pentagonal (Set.Ici 0)
have apply : ∀ (a : ℤ),
  ¬IsMax a →
    Membership.mem (γ := Set ℤ) (Set.Ici 0) a →
      Membership.mem (γ := Set ℤ) (Set.Ici 0) (a + 1) → pentagonal a < pentagonal (a + 1)
Tactic: apply strictMonoOn_of_lt_add_one Set.ordConnected_Ici
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Pentagonal (goal)
Goal:
⊢ StrictAntiOn pentagonal (Set.Iic 0)
have apply : ∀ (a : ℤ),
  ¬IsMax a →
    Membership.mem (γ := Set ℤ) (Set.Iic 0) a →
      Membership.mem (γ := Set ℤ) (Set.Iic 0) (a + 1) → pentagonal (a + 1) < pentagonal a
Tactic: apply strictAntiOn_of_add_one_lt Set.ordConnected_Iic
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
h : n + 2 ≠ 0
⊢ Even (n + 2).largeSchroder
have rw : Even ((n + 1).largeSchroder + ∑ i ∈ Iic (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder)
Tactic: rw [largeSchroder_succ]
-- Lean 4 proof step from Mathlib.Combinatorics.Enumerative.Schroder (goal)
Goal:
n : ℕ
h : n + 2 ≠ 0
⊢ Even ((n + 1).largeSchroder + ∑ i ∈ Iic (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder)
have refine : ∀ (k : ℕ) (hk : k ∈ Iic (n + 1)), Even (k.largeSchroder * (n + 1 - k).largeSchroder)
Tactic: refine .add (even_largeSchroder n.succ_ne_zero) <| even_sum _ fun k hk ↦ ?_