awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
suffices : cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p
⊢ cyclotomic (n * p) R = HPow.hPow (α := R[X]) (cyclotomic n R) p

Tactic:
suffices cyclotomic (n * p) (ZMod p) = cyclotomic n (ZMod p) ^ p by
    rw [← map_cyclotomic _ (algebraMap (ZMod p) R), ← map_cyclotomic _ (algebraMap (ZMod p) R),
      this, Polynomial.map_pow]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p n : ℕ
hp : Fact (Nat.Prime p)
inst : Ring R
inst_1 : CharP R p
hn : p ∣ n
this : Algebra (ZMod p) R := ZMod.algebra R p
rw :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (cyclotomic n (ZMod p)))
rw₁ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (cyclotomic n ℤ)))
rw₂ :
  Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p))
    (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (cyclotomic n ℤ)))
rw₃ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (map (Int.castRingHom (ZMod p)) (cyclotomic (n * p) ℤ))
rw₄ rw₅ : Eq (α := (ZMod p)[X]) (cyclotomic (n * p) (ZMod p)) (cyclotomic (n * p) (ZMod p))
⊢ cyclotomic (n * p) (ZMod p) = HPow.hPow (α := (ZMod p)[X]) (cyclotomic n (ZMod p)) p

Tactic:
rw [← ZMod.expand_card, ← map_cyclotomic_int n, ← map_expand,
    cyclotomic_expand_eq_cyclotomic hp.out hn, map_cyclotomic]

Premises used: Polynomial.map_expand, Polynomial.map_cyclotomic_int, ZMod.expand_card, Polynomial.map_cyclotomic, Polynomial.cyclotomic_expand_eq_cyclotomic, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
h : LT.lt (α := ℕ) 0 1
rw : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - p ^ HSub.hSub (α := ℕ) 1 1)
rw₁ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - HPow.hPow (β := ℕ) p 0)
rw₂ : cyclotomic (p * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
rw₃ : cyclotomic (m * p) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
rw₄ rw₅ : HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1) = HPow.hPow (α := R[X]) (cyclotomic m R) (p - 1)
⊢ cyclotomic (HPow.hPow (β := ℕ) p 1 * m) R =
    HPow.hPow (α := R[X]) (cyclotomic m R) (HPow.hPow (β := ℕ) p 1 - p ^ HSub.hSub (α := ℕ) 1 1)

Tactic:
rw [pow_one, Nat.sub_self, pow_zero, mul_comm, cyclotomic_mul_prime_eq_pow_of_not_dvd R hm]

Premises used: pow_zero, Nat.sub_self, Polynomial.cyclotomic_mul_prime_eq_pow_of_not_dvd, pow_one, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
rw : p ^ a.succ * m = p * p ^ a * m
rw₁ rw₂ : p * p ^ a * m = p * p ^ a * m
⊢ p ^ a.succ * m = p * (p ^ a * m)

Tactic:
rw [← mul_assoc, pow_succ']

Premises used: mul_assoc, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
⊢ p ∣ p ^ a.succ * m

Tactic:
have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ']⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
rw :
  HPow.hPow (α := R[X]) (cyclotomic m R) ((p ^ a.succ - p ^ (a.succ - 1)) * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ (a + 1) - p ^ (a + 2 - 1))
rw₁ : ¬p ∣ m
⊢ cyclotomic (p ^ (a + 2) * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p ^ (a + 2) - p ^ (a + 2 - 1))

Tactic:
rw [pow_succ', mul_assoc, mul_comm, cyclotomic_mul_prime_dvd_eq_pow R hdiv,
      cyclotomic_mul_prime_pow_eq _ _ a.succ_pos, ← pow_mul]

Premises used: mul_assoc, Polynomial.cyclotomic_mul_prime_dvd_eq_pow, pow_mul, Nat.succ_pos, mul_comm, pow_succ'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
simp :
  HPow.hPow (α := R[X]) (cyclotomic m R) ((p ^ a.succ - p ^ a) * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ (a + 1) - p ^ (a + 1))
⊢ HPow.hPow (α := R[X]) (cyclotomic m R) ((p ^ a.succ - p ^ (a.succ - 1)) * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ (a + 1) - p ^ (a + 2 - 1))

Tactic:
simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero]

Premises used: Nat.sub_zero, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
rw :
  HPow.hPow (α := R[X]) (cyclotomic m R) (p ^ a.succ * p - p ^ a * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ (a + 1) - p ^ (a + 1))
rw₁ :
  HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ a.succ - p ^ a * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ (a + 1) - p ^ (a + 1))
rw₂ rw₃ :
  HPow.hPow (α := R[X]) (cyclotomic m R) (p * (p ^ a * p) - p ^ a * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * (p ^ a * p) - p ^ a * p)
⊢ HPow.hPow (α := R[X]) (cyclotomic m R) ((p ^ a.succ - p ^ a) * p) =
    HPow.hPow (α := R[X]) (cyclotomic m R) (p * p ^ (a + 1) - p ^ (a + 1))

Tactic:
rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]

Premises used: pow_succ, Nat.mul_sub_right_distrib, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
R : Type u_1
p m : ℕ
inst : Fact (Nat.Prime p)
inst_1 : Ring R
inst_2 : CharP R p
hm : ¬p ∣ m
a : ℕ
h : 0 < a + 2
hdiv : p ∣ p ^ a.succ * m
⊢ ¬p ∣ m

Tactic:
assumption
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
inl : IsRoot (cyclotomic (HPow.hPow (β := ℕ) p 0 * m) R) μ ↔ IsPrimitiveRoot μ m
inr : ∀ (hk : k > 0), IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m

Tactic:
rcases k.eq_zero_or_pos with (rfl | hk)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
inl : IsRoot (cyclotomic (1 * m) R) μ ↔ IsPrimitiveRoot μ m
inl₁ : IsRoot (cyclotomic m R) μ ↔ IsPrimitiveRoot μ m
inl₂ inl₃ : IsPrimitiveRoot μ m ↔ IsPrimitiveRoot μ m
⊢ IsRoot (cyclotomic (HPow.hPow (β := ℕ) p 0 * m) R) μ ↔ IsPrimitiveRoot μ m

Tactic:
rw [pow_zero, one_mul, isRoot_cyclotomic_iff]

Premises used: pow_zero, one_mul, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
inr : ∀ (h : IsRoot (cyclotomic (p ^ k * m) R) μ), IsPrimitiveRoot μ m
inr₁ : ∀ (h : IsPrimitiveRoot μ m), IsRoot (cyclotomic (p ^ k * m) R) μ
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : IsRoot (cyclotomic (p ^ k * m) R) μ
⊢ eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0

Tactic:
rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow]
      at h

Premises used: NeZero.not_char_dvd, Polynomial.eval_pow, Polynomial.IsRoot.def, Polynomial.cyclotomic_mul_prime_pow_eq
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : eval μ (cyclotomic m R) ^ (p ^ k - p ^ (k - 1)) = 0
⊢ eval μ (cyclotomic m R) = 0

Tactic:
replace h := eq_zero_of_pow_eq_zero h
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : eval μ (cyclotomic m R) = 0
inr : ∀ (h : IsRoot (cyclotomic m R) μ), IsPrimitiveRoot μ m
inr₁ inr₂ inr₃ inr₄ : ∀ (h : IsPrimitiveRoot μ m), IsPrimitiveRoot μ m
⊢ IsPrimitiveRoot μ m

Tactic:
rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h

Premises used: Polynomial.IsRoot.def, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : IsPrimitiveRoot μ m
⊢ eval μ (cyclotomic m R) = 0

Tactic:
rw [← isRoot_cyclotomic_iff, IsRoot.def] at h

Premises used: Polynomial.IsRoot.def, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : eval μ (cyclotomic m R) = 0
inr : p ^ k - p ^ (k - 1) ≠ 0
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ

Tactic:
rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow,
      h, zero_pow]

Premises used: NeZero.not_char_dvd, Polynomial.eval_pow, Polynomial.IsRoot.def, Polynomial.cyclotomic_mul_prime_pow_eq, zero_pow
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ p ^ k - p ^ (k - 1) ≠ 0

Tactic:
Nat.sub_ne_zero_of_lt <| pow_right_strictMono₀ hp.out.one_lt <| Nat.pred_lt hk.ne'

Premises used: Nat.Prime.one_lt, LT.lt.ne', Nat.pred_lt, Nat.sub_ne_zero_of_lt, pow_right_strictMono₀, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
Goal:
m k p : ℕ
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
hp : Fact (Nat.Prime p)
hchar : CharP R p
μ : R
inst_2 : NeZero.{u_1} (R := R) (↑m : R)
hk : k > 0
h : eval μ (cyclotomic m R) = 0
⊢ p ^ k - p ^ (k - 1) ≠ 0

Tactic:
exact Nat.sub_ne_zero_of_lt <| pow_right_strictMono₀ hp.out.one_lt <| Nat.pred_lt hk.ne'

Premises used: Nat.Prime.one_lt, LT.lt.ne', Nat.pred_lt, Nat.sub_ne_zero_of_lt, pow_right_strictMono₀, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f : ℕ
hK : Fintype.card K = p ^ f
h0 : f = 0
⊢ Fintype.card K ≤ 1

Tactic:
simpa [h0] using hK.le

Premises used: Eq.le
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
⊢ Fact (Irreducible P)

Tactic:
have : Fact (Irreducible P) := ⟨hPirr⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this : Fact (Irreducible P)
⊢ Module.Finite K (AdjoinRoot P)

Tactic:
have := hPmo.finite_adjoinRoot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this : Module.Finite K (AdjoinRoot P)
⊢ Finite.{u_1 + 1} (AdjoinRoot P)

Tactic:
have : Finite (AdjoinRoot P) := Module.finite_of_finite K
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this_3 : Finite.{u_1 + 1} (AdjoinRoot P)
this : NeZero.{u_1} (R := K) (↑n : K)
⊢ NeZero.{u_1} (R := AdjoinRoot P) (↑n : AdjoinRoot P)

Tactic:
simpa using NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective

Premises used: AdjoinRoot, Algebra.algebraMap, RingHom.injective, NeZero.of_injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
suffices : NeZero.{u_1} (R := K) (↑n : K)
⊢ NeZero.{u_1} (R := AdjoinRoot P) (↑n : AdjoinRoot P)

Tactic:
suffices NeZero (n : K) by
        simpa using NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
⊢ CharP K p

Tactic:
have := charP_of_card_eq_prime_pow hK
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this_3 : Finite.{u_1 + 1} (AdjoinRoot P)
this : CharP K p
⊢ NeZero.{u_1} (R := K) (↑n : K)

Tactic:
⟨fun h0 ↦ Nat.Prime.not_coprime_iff_dvd.mpr
        ⟨p, hp.out, dvd_pow_self p (f_ne_zero hK), (CharP.cast_eq_zero_iff K p n).mp h0⟩
          (hn.pow_left f)⟩

Premises used: Iff.mpr, NeZero.mk, _private.0.Polynomial.f_ne_zero, Nat.Coprime.pow_left, dvd_pow_self, And.intro, Exists.intro, Iff.mp, CharP.cast_eq_zero_iff, Fact.out, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this_3 : Finite.{u_1 + 1} (AdjoinRoot P)
this : CharP K p
⊢ NeZero.{u_1} (R := K) (↑n : K)

Tactic:
exact ⟨fun h0 ↦ Nat.Prime.not_coprime_iff_dvd.mpr
        ⟨p, hp.out, dvd_pow_self p (f_ne_zero hK), (CharP.cast_eq_zero_iff K p n).mp h0⟩
          (hn.pow_left f)⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
⊢ NeZero.{u_1} (R := AdjoinRoot P) (↑n : AdjoinRoot P)

Tactic:
have : NeZero (n : AdjoinRoot P) := by
      suffices NeZero (n : K) by
        simpa using NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective
      have := charP_of_card_eq_prime_pow hK
      exact ⟨fun h0 ↦ Nat.Prime.not_coprime_iff_dvd.mpr
        ⟨p, hp.out, dvd_pow_self p (f_ne_zero hK), (CharP.cast_eq_zero_iff K p n).mp h0⟩
          (hn.pow_left f)⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this_3 : Finite.{u_1 + 1} (AdjoinRoot P)
this : NeZero.{u_1} (R := AdjoinRoot P) (↑n : AdjoinRoot P)
⊢ map (of P) P ∣ cyclotomic n (AdjoinRoot P)

Tactic:
simpa using map_dvd (algebraMap K (AdjoinRoot P)) hP

Premises used: AdjoinRoot, Algebra.algebraMap, Polynomial.map_dvd
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this_3 : Finite.{u_1 + 1} (AdjoinRoot P)
this : NeZero.{u_1} (R := AdjoinRoot P) (↑n : AdjoinRoot P)
⊢ IsPrimitiveRoot (root P) n

Tactic:
simpa [← isRoot_cyclotomic_iff] using (isRoot_root P).dvd
      (by simpa using map_dvd (algebraMap K (AdjoinRoot P)) hP)

Premises used: Polynomial.IsRoot.dvd, Polynomial.isRoot_cyclotomic_iff, AdjoinRoot.isRoot_root
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
⊢ IsPrimitiveRoot (root P) n

Tactic:
have hζ : IsPrimitiveRoot (root P) n := by
    have : NeZero (n : AdjoinRoot P) := by
      suffices NeZero (n : K) by
        simpa using NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective
      have := charP_of_card_eq_prime_pow hK
      exact ⟨fun h0 ↦ Nat.Prime.not_coprime_iff_dvd.mpr
        ⟨p, hp.out, dvd_pow_self p (f_ne_zero hK), (CharP.cast_eq_zero_iff K p n).mp h0⟩
          (hn.pow_left f)⟩
    simpa [← isRoot_cyclotomic_iff] using (isRoot_root P).dvd
      (by simpa using map_dvd (algebraMap K (AdjoinRoot P)) hP)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
rw :
  orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
rw [← powerBasis_dim hPirr.ne_zero, ← pB.finrank, ← orderOf_frobeniusAlgEquivOfAlgebraic]

Premises used: FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic, PowerBasis.finrank, AdjoinRoot.powerBasis_dim, Irreducible.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
h0 : n = 0
⊢ False

Tactic:
simp [h0, hp.out.ne_one] at hn

Premises used: Nat.Prime.ne_one, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
⊢ IsOfFinOrder (root P)

Tactic:
have hζ' := isOfFinOrder_iff_pow_eq_one.mpr
      ⟨n, pos_of_ne_zero (fun h0 ↦ by simp [h0, hp.out.ne_one] at hn),
      hζ.pow_eq_one⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
⊢ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
dvd_antisymm
    (orderOf_dvd_iff_pow_eq_one.mpr <| AlgEquiv.coe_algHom_injective <| pB.algHom_ext ?_)
    (orderOf_dvd_iff_pow_eq_one.mpr <| Units.ext ?_)

Premises used: Iff.mpr, dvd_antisymm, Units.ext, AlgEquiv.coe_algHom_injective, PowerBasis.algHom_ext, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this_1 : Fact (Irreducible P)
this_2 : Module.Finite K (AdjoinRoot P)
this : Finite.{u_1 + 1} (AdjoinRoot P)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
refine_1 :
  Eq (α := AdjoinRoot P)
    (((↑(HPow.hPow (α := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))
                (orderOf (unitOfCoprime (p ^ f) ⋯))) :
            AdjoinRoot P →ₐ[K] AdjoinRoot P) :
          (a : AdjoinRoot P) → AdjoinRoot P)
        pB.gen :
      AdjoinRoot P)
    (((↑1 : AdjoinRoot P →ₐ[K] AdjoinRoot P) : (a : AdjoinRoot P) → AdjoinRoot P) pB.gen : AdjoinRoot P)
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
⊢ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
refine dvd_antisymm
    (orderOf_dvd_iff_pow_eq_one.mpr <| AlgEquiv.coe_algHom_injective <| pB.algHom_ext ?_)
    (orderOf_dvd_iff_pow_eq_one.mpr <| Units.ext ?_)

Premises used: Iff.mpr, dvd_antisymm, Units.ext, AlgEquiv.coe_algHom_injective, PowerBasis.algHom_ext, orderOf_dvd_iff_pow_eq_one