awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ coeff (cyclotomic n R) 0 = 1
have hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
Tactic: have hprod : (∏ i ∈ Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 := by
    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]
    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))
    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)
    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]
    simp only [hrw, mul_one, zero_sub, coeff_one_zero, coeff_X_zero, coeff_sub]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₁ : coeff (∏ i ∈ cons n n.properDivisors sorry, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₂ : (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₂ :
  (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₃ : coeff (cyclotomic n R) 0 * coeff (∏ x ∈ n.properDivisors, cyclotomic x R) 0 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₂ :
  (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
rw₃ : coeff (cyclotomic n R) 0 * coeff (∏ x ∈ n.properDivisors, cyclotomic x R) 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₄ : coeff (cyclotomic n R) 0 * ∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₂ :
  (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
rw₃ : coeff (cyclotomic n R) 0 * coeff (∏ x ∈ n.properDivisors, cyclotomic x R) 0 = -coeff (cyclotomic n R) 0
rw₄ : coeff (cyclotomic n R) 0 * ∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₅ : coeff (cyclotomic n R) 0 * -1 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₂ :
  (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
rw₃ : coeff (cyclotomic n R) 0 * coeff (∏ x ∈ n.properDivisors, cyclotomic x R) 0 = -coeff (cyclotomic n R) 0
rw₄ : coeff (cyclotomic n R) 0 * ∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₅ : coeff (cyclotomic n R) 0 * -1 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₆ : -(coeff (cyclotomic n R) 0 * 1) = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
rw : coeff (∏ i ∈ n.divisors, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₁ : coeff (∏ i ∈ cons n n.properDivisors ⋯, cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₂ :
  (HMul.hMul (α := R[X]) (cyclotomic n R) (∏ x ∈ n.properDivisors, cyclotomic x R)).coeff 0 = -coeff (cyclotomic n R) 0
rw₃ : coeff (cyclotomic n R) 0 * coeff (∏ x ∈ n.properDivisors, cyclotomic x R) 0 = -coeff (cyclotomic n R) 0
rw₄ : coeff (cyclotomic n R) 0 * ∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0 = -coeff (cyclotomic n R) 0
rw₅ : coeff (cyclotomic n R) 0 * -1 = -coeff (cyclotomic n R) 0
rw₆ : -(coeff (cyclotomic n R) 0 * 1) = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
have rw₇ : -coeff (cyclotomic n R) 0 = -coeff (cyclotomic n R) 0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
⊢ coeff (cyclotomic n R) 0 = 1
have heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
Tactic: have heq : (X ^ n - 1 : R[X]).coeff 0 = -(cyclotomic n R).coeff 0 := by
    rw [← prod_cyclotomic_eq_X_pow_sub_one (zero_le_one.trans_lt hn), ←
      Nat.cons_self_properDivisors hn.ne_bot, Finset.prod_cons, mul_coeff_zero, coeff_zero_prod,
      hprod, mul_neg, mul_one]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
⊢ (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
have rw : eval 0 (HPow.hPow (α := R[X]) X n - 1) = -1
Tactic: rw [coeff_zero_eq_eval_zero _]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
⊢ coeff (cyclotomic n R) 0 = 1
have hzero : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
Tactic: have hzero : (X ^ n - 1 : R[X]).coeff 0 = (-1 : R) := by
    rw [coeff_zero_eq_eval_zero _]
    simp only [zero_pow (by positivity : n ≠ 0), eval_X, eval_one, zero_sub, eval_pow, eval_sub]
-- 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
hprod : Eq.{u_1 + 1} (α := R) (∏ i ∈ n.properDivisors, coeff (cyclotomic i R) 0) (-1)
heq : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -coeff (cyclotomic n R) 0
hzero : (HPow.hPow (α := R[X]) X n - 1).coeff 0 = -1
⊢ coeff (cyclotomic n R) 0 = 1
have heq₁ : -1 = -coeff (cyclotomic n R) 0
Tactic: rw [hzero] at heq
Cleared hypotheses: heq, hzero
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
⊢ a.Coprime p
have a₁ : p.Coprime a
Tactic: apply Nat.Coprime.symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
⊢ p.Coprime a
have a₁ : ¬p ∣ a
Tactic: rw [hprime.1.coprime_iff_not_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
h : p ∣ a
⊢ False
have h₁ : Eq (α := ZMod p) (↑a : ZMod p) 0
Tactic: replace h := (ZMod.natCast_eq_zero_iff a p).2 h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
h : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ False
have hroot₁ : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
Tactic: rw [IsRoot.def, eq_natCast, h, ← coeff_zero_eq_eval_zero] at hroot
Cleared hypotheses: hroot, h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ False
have pos : ∀ (hone : n = 1), False
Tactic: by_cases hone : n = 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
pos : ∀ (hone : n = 1), False
⊢ False
have neg : ∀ (hone : ¬n = 1), False
Tactic: by_cases hone : n = 1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
hprime : Fact (Nat.Prime p)
a : ℕ
hroot : Eq (α := ZMod p) (coeff (cyclotomic n (ZMod p)) 0) 0
h : Eq (α := ZMod p) (↑a : ZMod p) 0
hone : ¬n = 1
⊢ False
have hroot₁ : Eq (α := ZMod p) 1 0
Tactic: rw [cyclotomic_coeff_zero (ZMod p) (Nat.succ_le_of_lt
    (lt_of_le_of_ne (Nat.succ_le_of_lt hpos) (Ne.symm hone)))] at hroot
Cleared hypotheses: hroot, h, hone
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
⊢ orderOf (ZMod.unitOfCoprime a ⋯) ∣ n
have h : ZMod.unitOfCoprime a sorry ^ n = 1
Tactic: apply orderOf_dvd_of_pow_eq_one
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
hpow :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1
have hpow₁ : HPow.hPow (α := ZMod p) (↑a : ZMod p) n - 1 = 0
Tactic: simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow
Cleared hypotheses: hpow
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
hpow : HPow.hPow (α := ZMod p) (↑a : ZMod p) n - 1 = 0
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1
have apply : (↑(ZMod.unitOfCoprime a sorry ^ n) : ZMod p) = 1
Tactic: apply Units.val_eq_one.1
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1
have h : Eq (α := ZMod p)
  (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p) (0 : ZMod p)
Tactic: suffices hpow : eval (Nat.castRingHom (ZMod p) a) (X ^ n - 1 : (ZMod p)[X]) = 0 by
    simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow
    apply Units.val_eq_one.1
    simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  IsRoot (R := ZMod p) (cyclotomic n (ZMod p) : (ZMod p)[X]) ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a : ZMod p)
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have hroot₁ : Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p) (0 : ZMod p)
Tactic: rw [IsRoot.def] at hroot
Cleared hypotheses: hroot
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have h : Eq (α := ZMod p)
  (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) : ZMod p)
  (0 : ZMod p)
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)
h :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) : ZMod p)
    (0 : ZMod p)
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have h₁ : Eq (α := ZMod p)
  (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
      (∏ i ∈ Finset.cons n n.properDivisors sorry, cyclotomic i (ZMod p)) :
    ZMod p)
  (0 : ZMod p)
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)
h :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) : ZMod p)
    (0 : ZMod p)
h₁ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic i (ZMod p)) :
      ZMod p)
    (0 : ZMod p)
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have h₂ : Eq (α := ZMod p)
  (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
      (HMul.hMul (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p))) :
    ZMod p)
  (0 : ZMod p)
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)
h :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) : ZMod p)
    (0 : ZMod p)
h₁ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic i (ZMod p)) :
      ZMod p)
    (0 : ZMod p)
h₂ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (HMul.hMul (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p))) :
      ZMod p)
    (0 : ZMod p)
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have h₃ : HMul.hMul (α := ZMod p) (β := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p)) : ZMod p) =
  0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hpos : 0 < n
p : ℕ
inst : Fact (Nat.Prime p)
a : ℕ
hroot :
  Eq (α := ZMod p) (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
    (0 : ZMod p)
h :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ i ∈ n.divisors, cyclotomic i (ZMod p)) : ZMod p)
    (0 : ZMod p)
h₁ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (∏ i ∈ Finset.cons n n.properDivisors ⋯, cyclotomic i (ZMod p)) :
      ZMod p)
    (0 : ZMod p)
h₂ :
  Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a)
        (HMul.hMul (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p))) :
      ZMod p)
    (0 : ZMod p)
h₃ :
  HMul.hMul (α := ZMod p) (β := ZMod p)
      (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (cyclotomic n (ZMod p)) : ZMod p)
      (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p)) :
        ZMod p) =
    0
⊢ Eq (α := ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (HPow.hPow (α := (ZMod p)[X]) X n - 1) : ZMod p)
    (0 : ZMod p)
have h₄ : HMul.hMul (α := ZMod p) (β := ZMod p) (0 : ZMod p)
    (eval ((Nat.castRingHom (ZMod p) : (a : ℕ) → ZMod p) a) (∏ x ∈ n.properDivisors, cyclotomic x (ZMod p)) : ZMod p) =
  0
Tactic: rw [← prod_cyclotomic_eq_X_pow_sub_one hpos (ZMod p), ← Nat.cons_self_properDivisors hpos.ne',
    Finset.prod_cons, eval_mul, hroot, zero_mul]