awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    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 refine_2 : (↑(unitOfCoprime (p ^ f) sorry ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
    ZMod n) =
  1
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
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: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₂ : (↑(unitOfCoprime (p ^ f) sorry) : ZMod n) ^
    orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
  (↑1 : ZMod n)
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₃ : HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
    (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
  (↑1 : ZMod n)
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
refine_2₃ :
  HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
      (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
    (↑1 : ZMod n)
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₄ : Eq (α := ZMod n)
  (↑((p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
    ZMod n)
  (↑1 : ZMod n)
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
refine_2₃ :
  HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
      (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
    (↑1 : ZMod n)
refine_2₄ :
  Eq (α := ZMod n)
    (↑((p ^ f) ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n)
    (↑1 : ZMod n)
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₅ : (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
  1 [MOD n]
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
refine_2₃ :
  HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
      (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
    (↑1 : ZMod n)
refine_2₄ :
  Eq (α := ZMod n)
    (↑((p ^ f) ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n)
    (↑1 : ZMod n)
refine_2₅ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD n]
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₆ : (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
  1 [MOD orderOf (root P)]
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
refine_2₃ :
  HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
      (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
    (↑1 : ZMod n)
refine_2₄ :
  Eq (α := ZMod n)
    (↑((p ^ f) ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n)
    (↑1 : ZMod n)
refine_2₅ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD n]
refine_2₆ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD orderOf (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 refine_2₇ : root P ^
    (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
  HPow.hPow (β := ℕ) (root P) 1
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
refine_2₃ :
  HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
      (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
    (↑1 : ZMod n)
refine_2₄ :
  Eq (α := ZMod n)
    (↑((p ^ f) ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n)
    (↑1 : ZMod n)
refine_2₅ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD n]
refine_2₆ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD orderOf (root P)]
refine_2₇ :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    HPow.hPow (β := ℕ) (root P) 1
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₈ : root P = HPow.hPow (β := ℕ) (root P) 1
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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_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 :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    root P
refine_2 :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    1
refine_2₁ :
  (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
refine_2₂ :
  (↑(unitOfCoprime (p ^ f) ⋯) : ZMod n) ^
      orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    (↑1 : ZMod n)
refine_2₃ :
  HPow.hPow (α := ZMod n) (↑(p ^ f) : ZMod n)
      (orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) =
    (↑1 : ZMod n)
refine_2₄ :
  Eq (α := ZMod n)
    (↑((p ^ f) ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n)
    (↑1 : ZMod n)
refine_2₅ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD n]
refine_2₆ :
  (p ^ f) ^ orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) ≡
    1 [MOD orderOf (root P)]
refine_2₇ :
  root P ^
      (p ^ f) ^
        orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K)) =
    HPow.hPow (β := ℕ) (root P) 1
refine_2₈ : root P = HPow.hPow (β := ℕ) (root P) 1
⊢ (↑(unitOfCoprime (p ^ f) ⋯ ^
          orderOf (G := Gal(AdjoinRoot P/K)) (frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P) : Gal(AdjoinRoot P/K))) :
      ZMod n) =
    (↑1 : ZMod n)
have refine_2₉ : root P = root P
Tactic: rw [Units.val_one, ← Nat.cast_one, Units.val_pow_eq_pow_val, coe_unitOfCoprime,
      ← Nat.cast_pow, natCast_eq_natCast_iff, hζ.eq_orderOf, ← hζ'.pow_eq_pow_iff_modEq, this,
      pow_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
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have obtain : ∀ (A : K[X]) (hA : cyclotomic n K = P * A), P.natDegree = orderOf (unitOfCoprime (p ^ f) sorry)
Tactic: obtain ⟨A, hA⟩ := hP
Cleared hypotheses: 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) ∣ cyclotomic n K
have refine : cyclotomic n K =
  HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) *
    HMul.hMul (β := K[X]) A ((C : (a : K) → K[X]) P.leadingCoeff : K[X])
Tactic: refine ⟨A * C P.leadingCoeff, ?_⟩
-- 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ cyclotomic n K =
    HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) *
      HMul.hMul (β := K[X]) A ((C : (a : K) → K[X]) P.leadingCoeff : K[X])
have _ : P * A =
  P *
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X])
        ((C : (a : K) → K[X]) P.leadingCoeff : K[X]) *
    A
Tactic: calc
      _ = P * A := hA
      _ = P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A := by
        simp [← C_mul, leadingCoeff_ne_zero.mpr hPirr.ne_zero]
      _ = _ := by ring
-- 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
_ :
  P * A =
    P *
        HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X])
          ((C : (a : K) → K[X]) P.leadingCoeff : K[X]) *
      A
⊢ cyclotomic n K =
    HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) *
      HMul.hMul (β := K[X]) A ((C : (a : K) → K[X]) P.leadingCoeff : K[X])
have _₁ : P *
      HMul.hMul (α := K[X]) (β := K[X]) ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X])
        ((C : (a : K) → K[X]) P.leadingCoeff : K[X]) *
    A =
  HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) *
    HMul.hMul (β := K[X]) A ((C : (a : K) → K[X]) P.leadingCoeff : K[X])
Tactic: calc
      _ = P * A := hA
      _ = P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A := by
        simp [← C_mul, leadingCoeff_ne_zero.mpr hPirr.ne_zero]
      _ = _ := by ring