awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hcycl : P = cyclotomic n R
refine_1 :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) = HPow.hPow (α := R[X]) X n - 1
refine_1₁ :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) = ∏ i ∈ n.divisors, cyclotomic i R
refine_1₂ :
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) =
    ∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R
⊢ P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
have refine_1₃ : HMul.hMul (α := R[X]) (cyclotomic n R) (∏ i ∈ n.properDivisors, cyclotomic i R) =
  HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)
Tactic: rw [hcycl, ← prod_cyclotomic_eq_X_pow_sub_one hpos R, ← Nat.cons_self_properDivisors hpos.ne',
      Finset.prod_cons]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
⊢ Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
have hs : ∀ i ∈ n.properDivisors, Monic (cyclotomic i R)
Tactic: apply monic_prod_of_monic
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
⊢ P = cyclotomic n R
have prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
Tactic: have prod_monic : (∏ i ∈ Nat.properDivisors n, cyclotomic i R).Monic := by
      apply monic_prod_of_monic
      intro i _
      exact cyclotomic.monic i R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ P = cyclotomic n R
have rw : 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1 ∧
  degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
Tactic: rw [@cyclotomic_eq_X_pow_sub_one_div R _ _ hpos, (div_modByMonic_unique P 0 prod_monic _).1]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1
have rwa : (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1
Tactic: rwa [zero_add, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ 0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * P = HPow.hPow (α := R[X]) X n - 1 ∧
    degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
have refine : degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
Tactic: refine ⟨by rwa [zero_add, mul_comm], ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hpos : 0 < n
P : R[X]
h : Nontrivial R
hP : P * ∏ i ∈ n.properDivisors, cyclotomic i R = HPow.hPow (α := R[X]) X n - 1
prod_monic : Monic.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
⊢ degree.{u_1} (R := R) 0 < degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R)
have rw : degree.{u_1} (R := R) (∏ i ∈ n.properDivisors, cyclotomic i R) ≠ ⊥
Tactic: rw [degree_zero, bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
⊢ Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
have this : Eq (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) (cyclotomic (p ^ (m + 1)) R) ↔
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
      (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
    HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
Tactic: have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i)
      (pow_pos hp.pos (m + 1))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  Eq (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) (cyclotomic (p ^ (m + 1)) R) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
⊢ Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
have this₁ : Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
      (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
    HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
Tactic: rw [eq_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
⊢ Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
have rw : HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
      (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
    HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1 ↔
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
      (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
Tactic: rw [this, Nat.prod_properDivisors_prime_pow hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
m : ℕ
this :
  Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
rw :
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ i ∈ (p ^ (m + 1)).properDivisors, cyclotomic i R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1 ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
⊢ Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
have rw₁ : HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1 ↔
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
      (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
Tactic: rw [this, Nat.prod_properDivisors_prime_pow hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
⊢ Eq (α := R[X]) (cyclotomic (p ^ (n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n) ^ i)
have this : ∀ (m : ℕ),
  Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
    HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
        (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
      HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
Tactic: have : ∀ m, (cyclotomic (p ^ (m + 1)) R = ∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) ↔
      ((∑ i ∈ Finset.range p, (X ^ p ^ m) ^ i) *
        ∏ x ∈ Finset.range (m + 1), cyclotomic (p ^ x) R) = X ^ p ^ (m + 1) - 1 := by
    intro m
    have := eq_cyclotomic_iff (R := R) (P := ∑ i ∈ range p, (X ^ p ^ m) ^ i)
      (pow_pos hp.pos (m + 1))
    rw [eq_comm] at this
    rw [this, Nat.prod_properDivisors_prime_pow hp]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
⊢ Eq (α := R[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) R)
    (∑ i ∈ range p, HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 0) ^ i)
have this₁ : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
⊢ Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1 + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
have rw : HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
    (∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R) =
  HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
Tactic: rw [← (eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr ?_]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
⊢ HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
      (∏ i ∈ (p ^ (n_n + 1 + 1)).properDivisors, cyclotomic i R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
have rw : (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i) *
    HMul.hMul (α := R[X]) (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R)
      (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i) =
  HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
Tactic: rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
⊢ (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i) *
      HMul.hMul (α := R[X]) (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R)
        (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
have n_ih₁ : HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
    (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) =
  HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) - 1
Tactic: rw [this] at n_ih
Cleared hypotheses: n_ih
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
n_n : ℕ
n_ih :
  HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)
      (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) - 1
⊢ (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i) *
      HMul.hMul (α := R[X]) (∏ x ∈ range (n_n + 1), cyclotomic (p ^ x) R)
        (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i) =
    HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1)) - 1
have rw : HPow.hPow (α := R[X]) X (p ^ (n_n + 1) * p) = HPow.hPow (α := R[X]) X (p ^ (n_n + 1 + 1))
Tactic: rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
⊢ Eq (α := R[X]) (cyclotomic (p ^ (n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n) ^ i)
have zero : Eq (α := R[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) R)
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 0) ^ i)
Tactic: induction n with
  | zero => haveI := Fact.mk hp; simp [cyclotomic_prime]
  | succ n_n n_ih =>
    rw [← (eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr ?_]
    rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
    rw [this] at n_ih
    rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]
    simp only [pow_add, pow_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p n : ℕ
hp : Nat.Prime p
this :
  ∀ (m : ℕ),
    Eq (α := R[X]) (cyclotomic (p ^ (m + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i) ↔
      HMul.hMul (α := R[X]) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ m) ^ i)
          (∏ x ∈ range (m + 1), cyclotomic (p ^ x) R) =
        HPow.hPow (α := R[X]) X (p ^ (m + 1)) - 1
zero :
  Eq (α := R[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) R)
    (∑ i ∈ range p, HPow.hPow (α := R[X]) X (HPow.hPow (β := ℕ) p 0) ^ i)
⊢ Eq (α := R[X]) (cyclotomic (p ^ (n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n) ^ i)
have succ : ∀ (n_n : ℕ)
  (n_ih : Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ n_n) ^ i)),
  Eq (α := R[X]) (cyclotomic (p ^ (n_n + 1 + 1)) R) (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ (n_n + 1)) ^ i)
Tactic: induction n with
  | zero => haveI := Fact.mk hp; simp [cyclotomic_prime]
  | succ n_n n_ih =>
    rw [← (eq_cyclotomic_iff (pow_pos hp.pos (n_n + 1 + 1)) _).mpr ?_]
    rw [Nat.prod_properDivisors_prime_pow hp, Finset.prod_range_succ, n_ih]
    rw [this] at n_ih
    rw [mul_comm _ (∑ i ∈ _, _), n_ih, geom_sum_mul, sub_left_inj, ← pow_mul]
    simp only [pow_add, pow_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
⊢ cyclotomic (p ^ (k + 1)) R * (HPow.hPow (α := R[X]) X (p ^ k) - 1) = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
have rw : (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ k) ^ i) * (HPow.hPow (α := R[X]) X (p ^ k) - 1) =
  HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
Tactic: rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
rw :
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ k) ^ i) * (HPow.hPow (α := R[X]) X (p ^ k) - 1) =
    HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
⊢ cyclotomic (p ^ (k + 1)) R * (HPow.hPow (α := R[X]) X (p ^ k) - 1) = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
have rw₁ : HPow.hPow (α := R[X]) X (p ^ k) ^ p - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
Tactic: rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
rw :
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ k) ^ i) * (HPow.hPow (α := R[X]) X (p ^ k) - 1) =
    HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₁ : HPow.hPow (α := R[X]) X (p ^ k) ^ p - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
⊢ cyclotomic (p ^ (k + 1)) R * (HPow.hPow (α := R[X]) X (p ^ k) - 1) = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
have rw₂ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
Tactic: rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
rw :
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ k) ^ i) * (HPow.hPow (α := R[X]) X (p ^ k) - 1) =
    HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₁ : HPow.hPow (α := R[X]) X (p ^ k) ^ p - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₂ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
⊢ cyclotomic (p ^ (k + 1)) R * (HPow.hPow (α := R[X]) X (p ^ k) - 1) = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
have rw₃ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ k * p) - 1
Tactic: rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
p k : ℕ
hn : Fact (Nat.Prime p)
rw :
  (∑ i ∈ range p, HPow.hPow (α := R[X]) X (p ^ k) ^ i) * (HPow.hPow (α := R[X]) X (p ^ k) - 1) =
    HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₁ : HPow.hPow (α := R[X]) X (p ^ k) ^ p - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₂ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
rw₃ : HPow.hPow (α := R[X]) X (p ^ k * p) - 1 = HPow.hPow (α := R[X]) X (p ^ k * p) - 1
⊢ cyclotomic (p ^ (k + 1)) R * (HPow.hPow (α := R[X]) X (p ^ k) - 1) = HPow.hPow (α := R[X]) X (p ^ (k + 1)) - 1
have rw₄ : HPow.hPow (α := R[X]) X (p * p ^ k) - 1 = HPow.hPow (α := R[X]) X (p * p ^ k) - 1
Tactic: rw [cyclotomic_prime_pow_eq_geom_sum hn.out, geom_sum_mul, ← pow_mul, pow_succ, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hn : 1 < n
⊢ coeff (cyclotomic n R) 0 = 1
have h : ∀ (n : ℕ) (hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1) (hn : 1 < n), coeff (cyclotomic n R) 0 = 1
Tactic: induction n using Nat.strong_induction_on with | _ n hi
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
have rw : (HSub.hSub (α := R[X]) X 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0 = -1
Tactic: rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2
      (lt_of_lt_of_le one_lt_two hn)), Finset.prod_insert (Finset.notMem_erase 1 _),
      cyclotomic_one R]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
⊢ (HSub.hSub (α := R[X]) X 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0 = -1
have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
Tactic: have hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j := by
      intro j hj
      apply Nat.succ_le_of_lt
      exact (Ne.le_iff_lt (Finset.mem_erase.1 hj).1.symm).mp
        (Nat.succ_le_of_lt (Nat.pos_of_mem_properDivisors (Finset.mem_erase.1 hj).2))
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
⊢ (HSub.hSub (α := R[X]) X 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0 = -1
have hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
Tactic: have hcongr : ∀ j ∈ n.properDivisors.erase 1, (cyclotomic j R).coeff 0 = 1 := by
      intro j hj
      exact hi j (Nat.mem_properDivisors.1 (Finset.mem_erase.1 hj).2).2 (hleq j hj)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
⊢ Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0) 1
have rw : Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, 1) 1
Tactic: rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
hi : ∀ m < n, ∀ (hn : 1 < m), coeff (cyclotomic m R) 0 = 1
hn : 1 < n
hleq : ∀ j ∈ n.properDivisors.erase 1, 2 ≤ j
hcongr : ∀ j ∈ n.properDivisors.erase 1, coeff (cyclotomic j R) 0 = 1
⊢ (HSub.hSub (α := R[X]) X 1).coeff 0 * ∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0 = -1
have hrw : Eq.{u_1 + 1} (α := R) (∏ x ∈ n.properDivisors.erase 1, coeff (cyclotomic x R) 0) 1
Tactic: have hrw : (∏ x ∈ n.properDivisors.erase 1, (cyclotomic x R).coeff 0) = 1 := by
      rw [Finset.prod_congr (refl (n.properDivisors.erase 1)) hcongr]
      simp only [Finset.prod_const_one]