awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = pB.gen
⊢ 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)

Tactic:
simp only [AlgEquiv.coe_algHom, AlgEquiv.coe_pow, AlgEquiv.one_apply,
      coe_frobeniusAlgEquivOfAlgebraic, pow_iterate, hK]

Premises used: AlgEquiv.one_apply, pow_iterate, FiniteField.coe_frobeniusAlgEquivOfAlgebraic, AlgEquiv.coe_pow, AlgEquiv.coe_algHom
-- 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 : pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = HPow.hPow (β := ℕ) pB.gen 1
⊢ pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = pB.gen

Tactic:
nth_rewrite 2 [← pow_one pB.gen]

Premises used: PowerBasis.gen, pow_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 (α := ZMod n) (↑((p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯)) : ZMod n) (↑1 : ZMod n)
⊢ pB.gen ^ (p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯) = HPow.hPow (β := ℕ) pB.gen 1

Tactic:
rw [powerBasis_gen hPirr.ne_zero, hζ'.pow_eq_pow_iff_modEq, ← hζ.eq_orderOf,
      ← natCast_eq_natCast_iff]

Premises used: IsPrimitiveRoot.eq_orderOf, Irreducible.ne_zero, IsOfFinOrder.pow_eq_pow_iff_modEq, ZMod.natCast_eq_natCast_iff, AdjoinRoot.powerBasis_gen
-- 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)
⊢ Eq (α := ZMod n) (↑((p ^ f) ^ orderOf (unitOfCoprime (p ^ f) ⋯)) : ZMod n) (↑1 : ZMod n)

Tactic:
simpa only [Nat.cast_pow, Nat.cast_one, coe_unitOfCoprime, Units.val_one,
      Units.val_pow_eq_pow_val] using Units.val_inj.mpr <| pow_orderOf_eq_one
      (unitOfCoprime _ (hn.pow_left f))

Premises used: Iff.mpr, ZMod.unitOfCoprime, Nat.Coprime.pow_left, Units.val_inj, pow_orderOf_eq_one, Units.val_one, ZMod.coe_unitOfCoprime, Nat.cast_pow, Units.val_pow_eq_pow_val, Nat.cast_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)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
⊢ (φ ^ orderOf φ : (a : AdjoinRoot P) → AdjoinRoot P) (root P) = root P

Tactic:
simp [pow_orderOf_eq_one φ]

Premises used: pow_orderOf_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)
φ : Gal(AdjoinRoot P/K) := frobeniusAlgEquivOfAlgebraic K (AdjoinRoot P)
⊢ (φ ^ orderOf φ : (a : AdjoinRoot P) → AdjoinRoot P) (root P) = root P

Tactic:
have : (φ ^ orderOf φ) (root P) = root P := by simp [pow_orderOf_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_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
⊢ 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

Premises used: pow_iterate, FiniteField.coe_frobeniusAlgEquivOfAlgebraic, AlgEquiv.coe_pow
-- 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)
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
refine_2₉ refine_2₁₀ : 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)

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]

Premises used: IsPrimitiveRoot.eq_orderOf, pow_one, Units.val_one, IsOfFinOrder.pow_eq_pow_iff_modEq, ZMod.coe_unitOfCoprime, ZMod.natCast_eq_natCast_iff, Nat.cast_pow, Units.val_pow_eq_pow_val, Nat.cast_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
obtain : ∀ (A : K[X]) (hA : cyclotomic n K = P * A), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
obtain ⟨A, hA⟩ := 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)
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

Tactic:
⟨A * C P.leadingCoeff, ?_⟩

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, Exists.intro, DFunLike.coe
-- 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
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])
⊢ HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) ∣ cyclotomic n K

Tactic:
refine ⟨A * C P.leadingCoeff, ?_⟩
-- 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ cyclotomic n K = P * A

Tactic:
hA
-- 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)
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

Tactic:
simp [← C_mul, leadingCoeff_ne_zero.mpr hPirr.ne_zero]

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, Polynomial.C_mul, 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = 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 =
    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:
ring
-- 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)
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
_₁ :
  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])
⊢ 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:
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

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, Inv.inv, DFunLike.coe
-- 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)
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

Tactic:
have hQ : P * C P.leadingCoeff⁻¹ ∣ cyclotomic n K := by
    refine ⟨A * C P.leadingCoeff, ?_⟩
    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
-- 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)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
hQ : HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) ∣ cyclotomic n K
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
simpa [← natDegree_mul_leadingCoeff_self_inv P] using
    natDegree_of_dvd_cyclotomic_of_irreducible_of_monic hK hn hQ
    (irreducible_mul_leadingCoeff_inv.mpr hPirr) (monic_mul_leadingCoeff_inv hPirr.ne_zero)

Premises used: Iff.mpr, Polynomial.irreducible_mul_leadingCoeff_inv, _private.0.Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible_of_monic, Polynomial.natDegree_mul_leadingCoeff_self_inv, Polynomial.monic_mul_leadingCoeff_inv, 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ P ≠ 0

Tactic:
have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
obtain : ∀ (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Irreducible P
⊢ Irreducible P

Tactic:
obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..

Premises used: Polynomial.not_isUnit_of_natDegree_pos, orderOf_eq_zero_iff, UniqueFactorizationMonoid.exists_mem_normalizedFactors, isOfFinOrder_of_finite, pos_of_ne_zero, Iff.mp
-- 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ Irreducible P

Tactic:
(associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Associated.irreducible, Polynomial.associated_of_dvd_of_natDegree_le, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
refine : P.natDegree ≤ Q.natDegree
⊢ Irreducible P

Tactic:
refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)

Premises used: UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Associated.irreducible, Polynomial.associated_of_dvd_of_natDegree_le, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
rw : Q ∣ cyclotomic n K
⊢ P.natDegree ≤ Q.natDegree

Tactic:
rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]

Premises used: Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ Q ∣ cyclotomic n K

Tactic:
dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ

Premises used: Polynomial.cyclotomic_ne_zero, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Multiset.mem_of_le, Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ Q ∣ cyclotomic n K

Tactic:
exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ

Premises used: Polynomial.cyclotomic_ne_zero, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Multiset.mem_of_le, Iff.mp, UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
-- 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
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have have₁ have₂ : ∀ (hP0 : P ≠ 0), Irreducible P
have₃ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Irreducible P
have₄ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), P.natDegree ≤ Q.natDegree
have₅ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Q ∣ cyclotomic n K
⊢ Irreducible P

Tactic:
classical
  have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ

Premises used: Polynomial.not_isUnit_of_natDegree_pos, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, orderOf_eq_zero_iff, isOfFinOrder_of_finite, pos_of_ne_zero, Iff.mp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ Fintype.card (ZMod p) = HPow.hPow (β := ℕ) p 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ p.Coprime n

Tactic:
simpa using hp.1.coprime_iff_not_dvd.mpr hpn

Premises used: Iff.mpr, Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
p n : ℕ
hp : Fact (Nat.Prime p)
P : (ZMod p)[X]
hpn : ¬p ∣ n
hP : P ∣ cyclotomic n (ZMod p)
hPdeg : P.natDegree = orderOf (unitOfCoprime p ⋯)
⊢ P.natDegree = orderOf (unitOfCoprime (HPow.hPow (β := ℕ) p 1) ⋯)

Tactic:
simpa
-- 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)
inst_2 : DecidableEq K
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
natDegree_of_dvd_cyclotomic_of_irreducible hK hn (dvd_of_mem_normalizedFactors hP)
    (irreducible_of_normalized_factor P hP)

Premises used: Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, UniqueFactorizationMonoid.irreducible_of_normalized_factor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
⊢ Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)

Tactic:
have h := prod_normalizedFactors (cyclotomic_ne_zero n K)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
⊢ ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
have : ∀ P ∈ normalizedFactors (cyclotomic n K),
      P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f)) := fun P hP ↦
    natDegree_of_mem_normalizedFactors_cyclotomic hK hn hP
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ natDegree (prod (normalizedFactors (cyclotomic n K))) = natDegree (cyclotomic n K)

Tactic:
have H := natDegree_eq_of_degree_eq <| degree_eq_degree_of_associated h