-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem orderOf_root_cyclotomic_dvd {n : ℕ} (hpos : 0 < n) {p : ℕ} [Fact p.Prime] {a : ℕ}
    (hroot : IsRoot (cyclotomic n (ZMod p)) (Nat.castRingHom (ZMod p) a)) :
    orderOf (ZMod.unitOfCoprime a (coprime_of_root_cyclotomic hpos hroot)) ∣ n

Proof state:
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

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]

Result:
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0

Proof state:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
hpow : eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

Tactic:
simp only [eval_X, eval_one, eval_pow, eval_sub, eq_natCast] at hpow

Result:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

Proof state:
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 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]

Result:
no goals

Proof state:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ↑(ZMod.unitOfCoprime a ⋯ ^ n) = 1

Tactic:
simp only [sub_eq_zero.mp hpow, ZMod.coe_unitOfCoprime, Units.val_pow_eq_pow_val]

Result:
no goals

Proof state:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ orderOf (ZMod.unitOfCoprime a ⋯) ∣ n

Tactic:
apply orderOf_dvd_of_pow_eq_one

Result:
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

Proof state:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ZMod.unitOfCoprime a ⋯ ^ n = 1

Tactic:
apply Units.val_eq_one.1

Result:
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
hpow : ↑a ^ n - 1 = 0
⊢ ↑(ZMod.unitOfCoprime a ⋯ ^ n) = 1

Proof state:
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : (cyclotomic n (ZMod p)).IsRoot ((Nat.castRingHom (ZMod p)) a)
⊢ eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0

Tactic:
rw [IsRoot.def] at hroot

Result:
case h
n : ℕ
hpos : 0 < n
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℕ
hroot : eval ((Nat.castRingHom (ZMod p)) a) (cyclotomic n (ZMod p)) = 0
⊢ eval ((Nat.castRingHom (ZMod p)) a) (X ^ n - 1) = 0