awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
rw :
  Eq (α := (ZMod p)[X])
    ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) : (ZMod p)[X])
    (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q) : (ZMod p)[X])
⊢ HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)
have rw₁ : Eq (α := (ZMod p)[X])
  ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) : (ZMod p)[X])
  ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) : (ZMod p)[X])
Tactic: rw [← ZMod.expand_card, map_expand]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p
have hfrob : HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p =
  map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)
Tactic: have hfrob :
    map (Int.castRingHom (ZMod p)) Q ^ p = map (Int.castRingHom (ZMod p)) (expand ℤ p Q) := by
    rw [← ZMod.expand_card, map_expand]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob :
  HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p
have rw : Dvd.dvd (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
  (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q))
Tactic: rw [hfrob]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hfrob :
  HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)
⊢ Dvd.dvd (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
    (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q))
have apply : Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)
Tactic: apply _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
have pos : ∀ (hn : n = 0), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
pos : ∀ (hn : n = 0), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
have neg : ∀ (hn : ¬n = 0), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
have hpos : 0 < n
Tactic: have hpos := Nat.pos_of_ne_zero hn
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
have neg : ∀ (hdiff : ¬Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))), False
Tactic: by_contra hdiff
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
⊢ False
have Pmonic : P.Monic
Tactic: have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
⊢ False
have Qmonic : Q.Monic
Tactic: have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
⊢ False
have Pirr : Irreducible P
Tactic: have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
⊢ False
have PQprim : (P * Q).IsPrimitive
Tactic: have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ P * Q ∣ HPow.hPow (α := ℤ[X]) X n - 1
have rw : map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
Tactic: rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
        (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
      Polynomial.map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
have refine_1 : IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
Tactic: refine IsCoprime.mul_dvd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
refine_1 : IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
⊢ map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
have refine_2 : map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
Tactic: refine IsCoprime.mul_dvd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
refine_1 : IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
refine_2 : map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
have refine_3 : map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
Tactic: refine IsCoprime.mul_dvd ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
have aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
Tactic: have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)
have refine_1 : ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q
Tactic: refine (dvd_or_isCoprime _ _ (aux.1 Pirr)).resolve_left ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
⊢ ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q
have refine_1 : ¬P ∣ Q
Tactic: rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv_1 : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
aux : Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)
hdiv : P ∣ Q
⊢ False
have refine_1 : Associated P Q
Tactic: refine hdiff (eq_of_monic_of_associated Pmonic Qmonic ?_)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
have refine_2 : P ∣ HPow.hPow (α := ℤ[X]) X n - 1
Tactic: apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
have refine_3 : Q ∣ HPow.hPow (α := ℤ[X]) X n - 1
Tactic: apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
⊢ False
have prod : P * Q ∣ HPow.hPow (α := ℤ[X]) X n - 1
Tactic: have prod : P * Q ∣ X ^ n - 1 := by
    rw [IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast (P * Q) (X ^ n - 1) PQprim
        (monic_X_pow_sub_C (1 : ℤ) (ne_of_gt hpos)).isPrimitive,
      Polynomial.map_mul]
    refine IsCoprime.mul_dvd ?_ ?_ ?_
    · have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
      refine (dvd_or_isCoprime _ _ (aux.1 Pirr)).resolve_left ?_
      rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]
      intro hdiv
      refine hdiff (eq_of_monic_of_associated Pmonic Qmonic ?_)
      exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)
    · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2
      exact minpoly_dvd_x_pow_sub_one h
    · apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2
      exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod : P * Q ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ False
have prod₁ : Dvd.dvd (α := (ZMod p)[X]) ((mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (P * Q) : (ZMod p)[X])
  ((mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (HPow.hPow (α := ℤ[X]) X n - 1) : (ZMod p)[X])
Tactic: replace prod := _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
Cleared hypotheses: prod
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod :
  Dvd.dvd (α := (ZMod p)[X]) ((mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (P * Q) : (ZMod p)[X])
    ((mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (HPow.hPow (α := ℤ[X]) X n - 1) : (ZMod p)[X])
⊢ False
have prod₁ : HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P) (map (Int.castRingHom (ZMod p)) Q) ∣
  HPow.hPow (α := (ZMod p)[X]) X n - 1
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one,
    Polynomial.map_pow, map_X] at prod
Cleared hypotheses: prod
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod :
  HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P) (map (Int.castRingHom (ZMod p)) Q) ∣
    HPow.hPow (α := (ZMod p)[X]) X n - 1
⊢ False
have neg : ∀ (R : (ZMod p)[X])
  (hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R), False
Tactic: obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
prod :
  HMul.hMul (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P) (map (Int.castRingHom (ZMod p)) Q) ∣
    HPow.hPow (α := (ZMod p)[X]) X n - 1
R : (ZMod p)[X]
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
have prod₁ : HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
Tactic: rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod
Cleared hypotheses: prod, hR
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
w : (ZMod p)[X]
⊢ HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 ∣
    HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R
have h₁ : HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R =
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R
Tactic: use R
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
⊢ False
have habs : HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 ∣
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R
Tactic: have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by
    use R
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 ∣
    HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R
⊢ False
have habs₁ : (↑1 : ℕ∞) < emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1)
Tactic: replace habs :=
    lt_of_lt_of_le (Nat.cast_lt.2 one_lt_two)
      (le_emultiplicity_of_pow_dvd (dvd_trans habs prod))
Cleared hypotheses: habs
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : (↑1 : ℕ∞) < emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1)
⊢ False
have hfree : Squarefree (HPow.hPow (α := (ZMod p)[X]) X n - 1)
Tactic: have hfree : Squarefree (X ^ n - 1 : (ZMod p)[X]) :=
    (separable_X_pow_sub_C 1 (fun h => hdiv <| (ZMod.natCast_eq_zero_iff n p).1 h)
        one_ne_zero).squarefree
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hprime : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hn : ¬n = 0
hpos : 0 < n
P : ℤ[X] := minpoly ℤ μ
Q : ℤ[X] := minpoly ℤ (μ ^ p)
hdiff : ¬P = Q
Pmonic : P.Monic
Qmonic : Q.Monic
Pirr : Irreducible P
Qirr : Irreducible Q
PQprim : (P * Q).IsPrimitive
R : (ZMod p)[X]
prod :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R
habs : (↑1 : ℕ∞) < emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1)
hfree : Squarefree (HPow.hPow (α := (ZMod p)[X]) X n - 1)
⊢ False
have neg : ∀ (hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1), False
Tactic: rcases (squarefree_iff_emultiplicity_le_one (X ^ n - 1)).1 hfree
      (map (Int.castRingHom (ZMod p)) P) with hle | hunit