awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ p ^ a.succ * m = p * (p ^ a * m)
have rw₁ : p * p ^ a * m = p * p ^ a * m
Tactic: rw [← mul_assoc, pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
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
⊢ cyclotomic (p ^ (a + 2) * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p ^ (a + 2) - p ^ (a + 2 - 1))
have hdiv : p ∣ p ^ a.succ * m
Tactic: have hdiv : p ∣ p ^ a.succ * m := ⟨p ^ a * m, by rw [← mul_assoc, pow_succ']⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ cyclotomic (p ^ (a + 2) * m) R = HPow.hPow (α := R[X]) (cyclotomic m R) (p ^ (a + 2) - p ^ (a + 2 - 1))
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ 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))
have 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))
Tactic: simp only [Nat.succ_sub_succ_eq_sub, Nat.sub_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ 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))
have 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))
Tactic: rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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))
⊢ 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))
have 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))
Tactic: rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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))
⊢ 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))
have 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)
Tactic: rw [Nat.mul_sub_right_distrib, mul_comm, pow_succ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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)
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
have inl : IsRoot (cyclotomic (HPow.hPow (β := ℕ) p 0 * m) R) μ ↔ IsPrimitiveRoot μ m
Tactic: rcases k.eq_zero_or_pos with (rfl | hk)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
have inr : ∀ (hk : k > 0), IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
Tactic: rcases k.eq_zero_or_pos with (rfl | hk)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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)
⊢ IsRoot (cyclotomic (HPow.hPow (β := ℕ) p 0 * m) R) μ ↔ IsPrimitiveRoot μ m
have inl : IsRoot (cyclotomic (1 * m) R) μ ↔ IsPrimitiveRoot μ m
Tactic: rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsRoot (cyclotomic (HPow.hPow (β := ℕ) p 0 * m) R) μ ↔ IsPrimitiveRoot μ m
have inl₁ : IsRoot (cyclotomic m R) μ ↔ IsPrimitiveRoot μ m
Tactic: rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsRoot (cyclotomic (HPow.hPow (β := ℕ) p 0 * m) R) μ ↔ IsPrimitiveRoot μ m
have inl₂ : IsPrimitiveRoot μ m ↔ IsPrimitiveRoot μ m
Tactic: rw [pow_zero, one_mul, isRoot_cyclotomic_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
have inr : ∀ (h : IsRoot (cyclotomic (p ^ k * m) R) μ), IsPrimitiveRoot μ m
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ ↔ IsPrimitiveRoot μ m
have inr₁ : ∀ (h : IsPrimitiveRoot μ m), IsRoot (cyclotomic (p ^ k * m) R) μ
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
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) μ
⊢ IsPrimitiveRoot μ m
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
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
⊢ IsPrimitiveRoot μ m
have h₁ : eval μ (cyclotomic m R) = 0
Tactic: replace h := eq_zero_of_pow_eq_zero h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsPrimitiveRoot μ m
have inr : ∀ (h : IsRoot (cyclotomic m R) μ), IsPrimitiveRoot μ m
Tactic: rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsPrimitiveRoot μ m
have inr₁ : ∀ (h : IsPrimitiveRoot μ m), IsPrimitiveRoot μ m
Tactic: rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (hypothesis)
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
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ
have h₁ : eval μ (cyclotomic m R) = 0
Tactic: rw [← isRoot_cyclotomic_iff, IsRoot.def] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Expand (goal)
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
⊢ IsRoot (cyclotomic (p ^ k * m) R) μ
have inr : p ^ k - p ^ (k - 1) ≠ 0
Tactic: rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow,
      h, zero_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have this : Fact (Irreducible P)
Tactic: have : Fact (Irreducible P) := ⟨hPirr⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have this₁ : Module.Finite K (AdjoinRoot P)
Tactic: have := hPmo.finite_adjoinRoot
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have this₁ : Finite.{u_1 + 1} (AdjoinRoot P)
Tactic: have : Finite (AdjoinRoot P) := Module.finite_of_finite K
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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)
have suffices : NeZero.{u_1} (R := K) (↑n : K)
Tactic: suffices NeZero (n : K) by
        simpa using NeZero.of_injective (algebraMap K (AdjoinRoot P)).injective
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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 := K) (↑n : K)
have this₁ : CharP K p
Tactic: have := charP_of_card_eq_prime_pow hK
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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
have this₁ : 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)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have hζ : 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)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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 ⋯
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have rw : orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
  orderOf (unitOfCoprime (p ^ f) sorry)
Tactic: rw [← powerBasis_dim hPirr.ne_zero, ← pB.finrank, ← orderOf_frobeniusAlgEquivOfAlgebraic]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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 ⋯
⊢ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    orderOf (unitOfCoprime (p ^ f) ⋯)
have hζ' : 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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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) ⋯)
have refine_1 : Eq (α := AdjoinRoot P)
  (((↑(HPow.hPow (α := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))
              (orderOf (unitOfCoprime (p ^ f) sorry))) :
          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)
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 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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)
⊢ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    orderOf (unitOfCoprime (p ^ f) ⋯)
have refine_2 : (↑(unitOfCoprime (p ^ f) sorry ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
    ZMod n) =
  (↑1 : ZMod n)
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 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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)
⊢ 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)
have refine_1 : pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) sorry) = pB.gen
Tactic: simp only [AlgEquiv.coe_algHom, AlgEquiv.coe_pow, AlgEquiv.one_apply,
      coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, hK]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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)
⊢ pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = pB.gen
have refine_1 : pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) sorry) = HPow.hPow (β := ℕ) pB.gen 1
Tactic: nth_rewrite 2 [← pow_one pB.gen]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
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)
⊢ pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = HPow.hPow (β := ℕ) pB.gen 1
have refine_1 : Eq (α := ZMod n) (↑((p ^ f) ^ orderOf (unitOfCoprime (p ^ f) sorry)) : ZMod n) (↑1 : ZMod n)
Tactic: rw [powerBasis_gen hPirr.ne_zero, hζ'.pow_eq_pow_iff_modEq, ← hζ.eq_orderOf,
      ← natCast_eq_natCast_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have this₁ : (φ ^ orderOf φ : (a : AdjoinRoot P) → AdjoinRoot P) (root P) = root P
Tactic: have : (φ ^ orderOf φ) (root P) = root P := by simp [pow_orderOf_eq_one φ]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
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)
hζ : IsPrimitiveRoot (root P) n
pB : PowerBasis K (AdjoinRoot P) := powerBasis ⋯
hζ' : IsOfFinOrder (root P)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
this : (φ ^ orderOf φ : (a : AdjoinRoot P) → AdjoinRoot P) (root P) = root P
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have this₁ : root P ^
    (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
  root P
Tactic: simp only [AlgEquiv.coe_pow, φ, coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, hK] at this
Cleared hypotheses: this