awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := ⋯
⊢ Eq (α := K) ((Polynomial.aeval (μ ^ p) : (a : ℤ[X]) → K) (minpoly ℤ (μ ^ p)) : K) (0 : K)

Tactic:
exact minpoly.aeval _ _

Premises used: minpoly.aeval
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
set :
  let Q : ℤ[X] := minpoly ℤ (μ ^ p);
  map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣
    HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p))) p

Tactic:
set Q := minpoly ℤ (μ ^ p)

Premises used: Int, minpoly, HPow.hPow
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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])
rw₁ 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])
⊢ HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)

Tactic:
rw [← ZMod.expand_card, map_expand]

Premises used: Polynomial.map_expand, ZMod.expand_card
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)
⊢ 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]
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)
rw :
  Dvd.dvd (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
    (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

Tactic:
rw [hfrob]
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)
apply : Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((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))

Tactic:
apply _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))

Premises used: ZMod, map_dvd, Int.castRingHom, Polynomial.mapRingHom
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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 (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)

Tactic:
minpoly_dvd_expand h hdiv

Premises used: IsPrimitiveRoot.minpoly_dvd_expand
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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 (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)

Tactic:
exact minpoly_dvd_expand h hdiv

Premises used: IsPrimitiveRoot.minpoly_dvd_expand
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Dvd.dvd (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
    (map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)))

Tactic:
(squarefree_minpoly_mod h hdiv).isRadical _ _ (minpoly_dvd_pow_mod h hdiv)

Premises used: IsPrimitiveRoot.minpoly_dvd_pow_mod, Squarefree.isRadical, IsPrimitiveRoot.squarefree_minpoly_mod
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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))
neg : ∀ (hn : ¬n = 0), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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))

Tactic:
simp_all
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ 0 < n

Tactic:
have hpos := Nat.pos_of_ne_zero hn
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
neg : ∀ (hdiff : ¬Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))), False
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))

Tactic:
by_contra hdiff
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
hdiff : ¬Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
⊢ let P : ℤ[X] := minpoly ℤ μ;
  ¬P = minpoly ℤ (μ ^ p)

Tactic:
set P := minpoly ℤ μ

Premises used: Int, minpoly
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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 ℤ μ
hdiff : ¬P = minpoly ℤ (μ ^ p)
⊢ let Q : ℤ[X] := minpoly ℤ (μ ^ p);
  ¬P = Q

Tactic:
set Q := minpoly ℤ (μ ^ p)

Premises used: Int, minpoly, HPow.hPow
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ P.Monic

Tactic:
have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Q.Monic

Tactic:
have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Irreducible P

Tactic:
have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ (P * Q).IsPrimitive

Tactic:
have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
rw : map (Int.castRingHom ℚ) P * map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ P * Q ∣ 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]

Premises used: Polynomial.map_mul, HMul.hMul, Polynomial.monic_X_pow_sub_C, HSub.hSub, ne_of_gt, Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast, HPow.hPow, Polynomial.Monic.isPrimitive, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)

Tactic:
IsCoprime.mul_dvd ?_ ?_ ?_

Premises used: IsCoprime.mul_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)
refine_3 : map (Int.castRingHom ℚ) Q ∣ 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)

Tactic:
refine IsCoprime.mul_dvd ?_ ?_ ?_

Premises used: IsCoprime.mul_dvd
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Irreducible P ↔ Irreducible (map (Int.castRingHom ℚ) P)

Tactic:
have aux := IsPrimitive.Int.irreducible_iff_irreducible_map_cast Pmonic.isPrimitive
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)

Tactic:
(dvd_or_isCoprime _ _ (aux.1 Pirr)).resolve_left ?_

Premises used: dvd_or_isCoprime, Or.resolve_left, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)
refine_1 : ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q
⊢ IsCoprime (map (Int.castRingHom ℚ) P) (map (Int.castRingHom ℚ) Q)

Tactic:
refine (dvd_or_isCoprime _ _ (aux.1 Pirr)).resolve_left ?_

Premises used: dvd_or_isCoprime, Or.resolve_left, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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)
refine_1 : ¬P ∣ Q
⊢ ¬map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) Q

Tactic:
rw [map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic]

Premises used: Rat, Int.castRingHom, Polynomial.map_dvd_map, Int.cast_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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

Tactic:
hdiff (eq_of_monic_of_associated Pmonic Qmonic ?_)

Premises used: Polynomial.eq_of_monic_of_associated
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
refine_1 : Associated P Q
⊢ False

Tactic:
refine hdiff (eq_of_monic_of_associated Pmonic Qmonic ?_)

Premises used: Polynomial.eq_of_monic_of_associated
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Associated P Q

Tactic:
associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)

Premises used: associated_of_dvd_dvd, Irreducible.dvd_symm
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Associated P Q

Tactic:
exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv)

Premises used: associated_of_dvd_dvd, Irreducible.dvd_symm
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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_2 : P ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ map (Int.castRingHom ℚ) P ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)

Tactic:
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Pmonic).2

Premises used: Iff.mpr, Rat, Int.castRingHom, Polynomial.map_dvd_map, Int.cast_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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 ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
minpoly_dvd_x_pow_sub_one h

Premises used: IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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 ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
exact minpoly_dvd_x_pow_sub_one h

Premises used: IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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_3 : Q ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ map (Int.castRingHom ℚ) Q ∣ map (Int.castRingHom ℚ) (HPow.hPow (α := ℤ[X]) X n - 1)

Tactic:
apply (map_dvd_map (Int.castRingHom ℚ) Int.cast_injective Qmonic).2

Premises used: Iff.mpr, Rat, Int.castRingHom, Polynomial.map_dvd_map, Int.cast_injective
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Q ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)

Premises used: Fact.out, IsPrimitiveRoot.pow_of_prime, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ Q ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
exact minpoly_dvd_x_pow_sub_one (pow_of_prime h hprime.1 hdiv)

Premises used: Fact.out, IsPrimitiveRoot.pow_of_prime, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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

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)
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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
⊢ 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
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
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])
⊢ 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

Premises used: Polynomial.map_one, Polynomial.map_mul, Polynomial.map_pow, Polynomial.map_X, Polynomial.coe_mapRingHom, Polynomial.map_sub