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 : 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)
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
⊢ 1 ≤ ((↑a : ℕ) + 1) * m

Tactic:
nlinarith
-- 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
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)
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
⊢ 1 ≤ ((↑b : ℕ) + 1) * m

Tactic:
nlinarith
-- 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
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 : ℕ)

Tactic:
rw [tsub_left_inj (by nlinarith) (by nlinarith), mul_left_inj' (hm.ne.symm), add_left_inj] at h

Premises used: Ne.symm, add_left_inj, tsub_left_inj, mul_left_inj', LT.lt.ne
-- 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
a b : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)
h : (↑a : ℕ) = (↑b : ℕ)
⊢ a = b

Tactic:
SetCoe.ext h

Premises used: SetCoe.ext
-- 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
a b : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)
h : (↑a : ℕ) = (↑b : ℕ)
⊢ a = b

Tactic:
exact SetCoe.ext h

Premises used: SetCoe.ext
-- 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
this : ∀ (i : ℕ), m ∣ i + 1 → ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
⊢ 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:
simpa
-- 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_2 : ∀ (i : ℕ), m ∣ i + 1 → ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
⊢ 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:
suffices ∀ (i : ℕ), m ∣ i + 1 → ∃ j ≠ 0, j * m - 1 = i by simpa
-- 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
i : ℕ
hi : m ∣ i + 1
refine_2 : ∀ (j : ℕ) (hj : i + 1 = m * j), ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i
⊢ ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i

Tactic:
obtain ⟨j, hj⟩ := dvd_def.mp hi

Premises used: dvd_def, Iff.mp
-- 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
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
⊢ j ≠ 0

Tactic:
grind
-- 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
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
refine_2 : j * m = i + 1
⊢ ∃ (j : ℕ), j ≠ 0 ∧ j * m - 1 = i

Tactic:
refine ⟨j, by grind, Nat.sub_eq_of_eq_add ?_⟩
-- 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
i : ℕ
hi : m ∣ i + 1
j : ℕ
hj : i + 1 = m * j
refine_2 : j * m = m * j
refine_2₁ refine_2₂ : j * m = j * m
⊢ j * m = i + 1

Tactic:
rw [hj, mul_comm m j]

Premises used: mul_comm
-- 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
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 + 1 = ((↑i : ℕ) + 1) * m

Tactic:
grind
-- 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
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 + 1 = ((↑i : ℕ) + 1) * m

Tactic:
have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind
-- 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
i : (↑(Function.mulSupport.{0, u_1} (M := R⟦X⟧) fun (i : ℕ) ↦ 1 - HPow.hPow (α := R⟦X⟧) X (i + 1) ^ m) : Type)
this : ((↑i : ℕ) + 1) * m - 1 + 1 = ((↑i : ℕ) + 1) * m
⊢ (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

Tactic:
simp [this, pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
m : ℕ
hm : 0 < m
h : Nontrivial R
x : TopologicalSpace R := ⊥
⊢ DiscreteTopology R

Tactic:
have _ : DiscreteTopology R := ⟨rfl⟩
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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
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))
⊢ 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))

Tactic:
rw [powerSeriesMk_card_restricted_eq_tprod R (¬ m ∣ ·)]

Premises used: Dvd.dvd, Nat.Partition.powerSeriesMk_card_restricted_eq_tprod, Not
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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
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))
⊢ 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_countRestricted_eq_tprod R hm]

Premises used: Nat.Partition.powerSeriesMk_card_countRestricted_eq_tprod
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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
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)))
⊢ 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:
apply mul_right_cancel₀ (tprod_one_sub_X_pow_ne_zero R)

Premises used: PowerSeries.WithPiTopology.tprod_one_sub_X_pow_ne_zero, mul_right_cancel₀
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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
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)))
⊢ 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:
rw [aux_mul_one_sub_X_pow R hm]

Premises used: _private.0.Nat.Partition.aux_mul_one_sub_X_pow
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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
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)))
⊢ ∏' (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 [← (multipliable_powerSeriesMk_card_countRestricted R m).tprod_mul
    (multipliable_one_sub_X_pow _)]

Premises used: Multipliable.tprod_mul, Nat.Partition.multipliable_powerSeriesMk_card_countRestricted, PowerSeries.WithPiTopology.multipliable_one_sub_X_pow
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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 : ℕ
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))
⊢ 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))

Tactic:
simp_rw [pow_mul, geom_sum_mul_neg]

Premises used: pow_mul, geom_sum_mul_neg
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
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 : ℕ), (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:
exact tprod_congr (fun i ↦ by simp_rw [pow_mul, geom_sum_mul_neg])

Premises used: tprod_congr
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
n m : ℕ
hm : 0 < m
⊢ #(restricted n fun (x : ℕ) ↦ ¬m ∣ x) = #(countRestricted n m)

Tactic:
simpa using PowerSeries.ext_iff.mp
    (powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted ℤ hm) n

Premises used: Int, Nat.Partition.powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted, Iff.mp, PowerSeries.ext_iff
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
n : ℕ
simp_rw : #(restricted n fun (x : ℕ) ↦ ¬2 ∣ x) = #(countRestricted n 2)
⊢ #(odds n) = #(distincts n)

Tactic:
simp_rw [← countRestricted_two, odds, even_iff_two_dvd]

Premises used: Nat.Partition.odds, Nat.Partition.countRestricted_two, even_iff_two_dvd
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
n : ℕ
⊢ LT.lt (α := ℕ) 0 2

Tactic:
norm_num
-- Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher
Goal:
n : ℕ
⊢ #(restricted n fun (x : ℕ) ↦ ¬2 ∣ x) = #(countRestricted n 2)

Tactic:
exact card_restricted_eq_card_countRestricted n (by norm_num)

Premises used: Nat.Partition.card_restricted_eq_card_countRestricted
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
⊢ pentagonal k = (k * (3 * k - 1) / 2).toNat

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
⊢ pentagonal (-k) = (k * (3 * k + 1) / 2).toNat

Tactic:
grind [pentagonal_def]

Premises used: pentagonal_def
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
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
negSucc : ∀ (a : ℕ), (↑(pentagonal (Int.negSucc a)) : ℤ) = Int.negSucc a * (3 * Int.negSucc a - 1) / 2
⊢ (↑(pentagonal k) : ℤ) = k * (3 * k - 1) / 2

Tactic:
rcases k with (_ | _) | _
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
⊢ (↑(pentagonal (Int.ofNat 0)) : ℤ) = Int.ofNat 0 * (3 * Int.ofNat 0 - 1) / 2

Tactic:
grind [pentagonal_def]

Premises used: pentagonal_def
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
n : ℕ
⊢ (↑(pentagonal (Int.ofNat (n + 1))) : ℤ) = Int.ofNat (n + 1) * (3 * Int.ofNat (n + 1) - 1) / 2

Tactic:
grind [pentagonal_def]

Premises used: pentagonal_def
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
a : ℕ
⊢ (↑(pentagonal (Int.negSucc a)) : ℤ) = Int.negSucc a * (3 * Int.negSucc a - 1) / 2

Tactic:
grind [pentagonal_def]

Premises used: pentagonal_def
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
rw : 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1)
⊢ HMul.hMul (α := ℤ) 2 (↑(pentagonal k) : ℤ) = k * (3 * k - 1)

Tactic:
rw [natCast_pentagonal]

Premises used: natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
⊢ Even (k * (3 * k - 1))

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
⊢ 2 * (k * (3 * k - 1) / 2) = k * (3 * k - 1)

Tactic:
exact Int.two_mul_ediv_two_of_even (by grind)

Premises used: Int.two_mul_ediv_two_of_even
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
⊢ HMul.hMul (α := ℤ) 2 (↑(pentagonal (-k)) : ℤ) = k * (3 * k + 1)

Tactic:
grind [two_mul_natCast_pentagonal]

Premises used: two_mul_natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
x y : ℤ
h : pentagonal x = pentagonal y
⊢ (3 * (x + y) - 1) * (x - y) = 0

Tactic:
grind [two_mul_natCast_pentagonal]

Premises used: two_mul_natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
x y : ℤ
h : pentagonal x = pentagonal y
⊢ (3 * (x + y) - 1) * (x - y) = 0

Tactic:
replace h : (3 * (x + y) - 1) * (x - y) = 0 := by grind [two_mul_natCast_pentagonal]
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
inl : 3 * (x + y) - 1 = 0 → x = y
inr : x - y = 0 → x = y
⊢ x = y

Tactic:
cases mul_eq_zero.mp h

Premises used: mul_eq_zero, Iff.mp
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h_1 : 3 * (x + y) - 1 = 0
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
x y : ℤ
h : (3 * (x + y) - 1) * (x - y) = 0
h_1 : x - y = 0
⊢ x = y

Tactic:
grind
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
x y : ℤ
⊢ pentagonal x = pentagonal y ↔ x = y

Tactic:
pentagonal_injective.eq_iff

Premises used: Function.Injective.eq_iff, pentagonal_injective
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
h : 0 < k
⊢ pentagonal k < pentagonal (-k)

Tactic:
grind [natCast_pentagonal]

Premises used: natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
k : ℤ
h : 0 ≤ k
⊢ pentagonal (-k) < pentagonal (k + 1)

Tactic:
grind [natCast_pentagonal]

Premises used: natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
apply :
  ∀ (a : ℤ),
    ¬IsMax a →
      Membership.mem (γ := Set ℤ) (Set.Ici 0) a →
        Membership.mem (γ := Set ℤ) (Set.Ici 0) (a + 1) → pentagonal a < pentagonal (a + 1)
⊢ StrictMonoOn pentagonal (Set.Ici 0)

Tactic:
apply strictMonoOn_of_lt_add_one Set.ordConnected_Ici

Premises used: strictMonoOn_of_lt_add_one, Set.ordConnected_Ici
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
⊢ ∀ (a : ℤ),
    ¬IsMax a →
      Membership.mem (γ := Set ℤ) (Set.Ici 0) a →
        Membership.mem (γ := Set ℤ) (Set.Ici 0) (a + 1) → pentagonal a < pentagonal (a + 1)

Tactic:
grind [natCast_pentagonal]

Premises used: natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
apply :
  ∀ (a : ℤ),
    ¬IsMax a →
      Membership.mem (γ := Set ℤ) (Set.Iic 0) a →
        Membership.mem (γ := Set ℤ) (Set.Iic 0) (a + 1) → pentagonal (a + 1) < pentagonal a
⊢ StrictAntiOn pentagonal (Set.Iic 0)

Tactic:
apply strictAntiOn_of_add_one_lt Set.ordConnected_Iic

Premises used: Set.ordConnected_Iic, strictAntiOn_of_add_one_lt
-- Module: Mathlib.Combinatorics.Enumerative.Pentagonal
Goal:
⊢ ∀ (a : ℤ),
    ¬IsMax a →
      Membership.mem (γ := Set ℤ) (Set.Iic 0) a →
        Membership.mem (γ := Set ℤ) (Set.Iic 0) (a + 1) → pentagonal (a + 1) < pentagonal a

Tactic:
grind [natCast_pentagonal]

Premises used: natCast_pentagonal
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
⊢ largeSchroder 0 = 1

Tactic:
simp [largeSchroder]

Premises used: Nat.largeSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
⊢ largeSchroder 1 = 2

Tactic:
simp [largeSchroder]

Premises used: Nat.largeSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
⊢ largeSchroder 2 = 6

Tactic:
simp [largeSchroder]

Premises used: Nat.largeSchroder
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
⊢ (n + 1).largeSchroder = n.largeSchroder + ∑ i ∈ Iic n, i.largeSchroder * (n - i).largeSchroder

Tactic:
simp [largeSchroder, ← Iio_add_one_eq_Iic, Nat.Iio_eq_range, ← Fin.sum_univ_eq_sum_range]

Premises used: Nat.largeSchroder, Fin.sum_univ_eq_sum_range, Finset.Iio_add_one_eq_Iic, Nat.Iio_eq_range
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
h : Ne (α := ℕ) 1 0
⊢ Even (largeSchroder 1)

Tactic:
simp
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
rw : Even ((n + 1).largeSchroder + ∑ i ∈ Iic (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder)
⊢ Even (n + 2).largeSchroder

Tactic:
rw [largeSchroder_succ]

Premises used: Nat.largeSchroder_succ
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
⊢ Even ((n + 1).largeSchroder + ∑ i ∈ Iic (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder)

Tactic:
.add (even_largeSchroder n.succ_ne_zero) <| even_sum _ fun k hk ↦ ?_

Premises used: Nat.succ_ne_zero, Finset.even_sum, Even.add
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
refine : ∀ (k : ℕ) (hk : k ∈ Iic (n + 1)), Even (k.largeSchroder * (n + 1 - k).largeSchroder)
⊢ Even ((n + 1).largeSchroder + ∑ i ∈ Iic (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder)

Tactic:
refine .add (even_largeSchroder n.succ_ne_zero) <| even_sum _ fun k hk ↦ ?_

Premises used: Finset.even_sum
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k ∈ Iic (n + 1)
zero : ∀ (hk : 0 ∈ Iic (n + 1)), Even (largeSchroder 0 * (n + 1 - 0).largeSchroder)
succ : ∀ (k : ℕ) (hk : k + 1 ∈ Iic (n + 1)), Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)
⊢ Even (k.largeSchroder * (n + 1 - k).largeSchroder)

Tactic:
obtain _ | k := k
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
hk : 0 ∈ Iic (n + 1)
⊢ Even (largeSchroder 0 * (n + 1 - 0).largeSchroder)

Tactic:
simpa using even_largeSchroder n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ k ≤ n

Tactic:
simp at hk
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k ≤ n
⊢ k < n + 1

Tactic:
lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
⊢ k < n + 1

Tactic:
have : k < n + 1 := by simp at hk; lia
-- Module: Mathlib.Combinatorics.Enumerative.Schroder
Goal:
n : ℕ
h : n + 2 ≠ 0
k : ℕ
hk : k + 1 ∈ Iic (n + 1)
this : k < n + 1
⊢ Even ((k + 1).largeSchroder * (n + 1 - (k + 1)).largeSchroder)

Tactic:
.mul_right (even_largeSchroder k.succ_ne_zero) _

Premises used: Even.mul_right, Nat.succ_ne_zero