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 : ℕ
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
neg :
  ∀ (R : (ZMod p)[X])
    (hR : map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R), False
⊢ False

Tactic:
obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv

Premises used: IsPrimitiveRoot.minpoly_dvd_mod_p
-- 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 :
  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
⊢ 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

Premises used: Polynomial.map_mul, mul_assoc, Polynomial.map_pow, sq
-- 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 :
  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
prod₁ :
  HPow.hPow (α := (ZMod p)[X]) (β := ℕ) (map (Int.castRingHom (ZMod p)) P) 2 * R ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ (μ ^ p)) = map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) * R

Tactic:
rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod

Premises used: Polynomial.map_mul, mul_assoc, Polynomial.map_pow, sq
-- 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
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]
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
⊢ 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:
use R
-- 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
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
⊢ 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
-- 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
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
⊢ (↑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))
-- 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
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)
⊢ 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
-- 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
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)
neg : ∀ (hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1), False
neg₁ : ∀ (hunit : IsUnit (M := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P)), False
⊢ False

Tactic:
rcases (squarefree_iff_emultiplicity_le_one (X ^ n - 1)).1 hfree
      (map (Int.castRingHom (ZMod p)) P) with hle | hunit

Premises used: HSub.hSub, ZMod, squarefree_iff_emultiplicity_le_one, HPow.hPow, Int.castRingHom, Iff.mp, Polynomial.map, 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
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)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1
⊢ 1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1)

Tactic:
rw [Nat.cast_one] at habs

Premises used: Nat.cast_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
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)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1
habs₁ : 1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1)
⊢ Squarefree (HPow.hPow (α := (ZMod p)[X]) X n - 1)

Tactic:
rw [Nat.cast_one] at habs

Premises used: Nat.cast_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
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)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1
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)
⊢ emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1

Tactic:
rw [Nat.cast_one] at habs

Premises used: Nat.cast_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
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)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1
⊢ False

Tactic:
hle.not_gt habs

Premises used: LE.le.not_gt
-- 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
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)
hle : emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1) ≤ 1
⊢ False

Tactic:
exact hle.not_gt habs

Premises used: LE.le.not_gt
-- 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
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)
hunit : IsUnit (M := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P)
⊢ degree (R := ZMod p) (map (Int.castRingHom (ZMod p)) P) = 0

Tactic:
replace hunit := degree_eq_zero_of_isUnit hunit
-- 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
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)
hunit : degree (R := ZMod p) (map (Int.castRingHom (ZMod p)) P) = 0
neg : ∀ (hunit : P.degree = 0), False
rw : Ne (α := ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) P.leadingCoeff : ZMod p) (0 : ZMod p)
⊢ False

Tactic:
rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit

Premises used: Polynomial.degree_map_eq_of_leadingCoeff_ne_zero, ZMod, Int.castRingHom
-- 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
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)
hunit : P.degree = 0
⊢ False

Tactic:
(minpoly.degree_pos (isIntegral h hpos)).ne' hunit

Premises used: minpoly.degree_pos, IsPrimitiveRoot.isIntegral, LT.lt.ne'
-- 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
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)
hunit : P.degree = 0
⊢ False

Tactic:
exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit

Premises used: minpoly.degree_pos, IsPrimitiveRoot.isIntegral, LT.lt.ne'
-- 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
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)
hunit : degree (R := ZMod p) (map (Int.castRingHom (ZMod p)) P) = 0
⊢ Ne (α := ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) P.leadingCoeff : ZMod p) (0 : ZMod p)

Tactic:
simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne, not_false_iff,
      one_ne_zero]

Premises used: Ne, eq_intCast, Polynomial.Monic.leadingCoeff, not_false_iff, one_ne_zero, Int.cast_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
m : ℕ
hcop : m.Coprime n
revert : ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : m.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))

Tactic:
revert n hcop
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n : ℕ
⊢ ∀ (h : IsPrimitiveRoot μ n) (hcop : m.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))

Tactic:
UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_

Premises used: UniqueFactorizationMonoid.induction_on_prime
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m : ℕ
refine_1 :
  ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : Nat.Coprime 0 n),
    Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (HPow.hPow (β := ℕ) μ 0))
refine_2 :
  ∀ {n : ℕ} (x : ℕ),
    IsUnit x → ∀ (h : IsPrimitiveRoot μ n) (hcop : x.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ x))
refine_3 :
  ∀ {n : ℕ} (a p : ℕ),
    a ≠ 0 →
      Prime p →
        (∀ (h : IsPrimitiveRoot μ n) (hcop : a.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ a))) →
          ∀ (h : IsPrimitiveRoot μ n) (hcop : (p * a).Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ (p * a)))
⊢ ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : m.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))

Tactic:
refine UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n : ℕ
h : IsPrimitiveRoot μ n
hn : Nat.Coprime 0 n
refine_1 : μ = HPow.hPow (β := ℕ) μ 0
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (HPow.hPow (β := ℕ) μ 0))

Tactic:
congr
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n : ℕ
h : IsPrimitiveRoot μ n
hn : Nat.Coprime 0 n
⊢ μ = HPow.hPow (β := ℕ) μ 0

Tactic:
simpa [(Nat.coprime_zero_left _).mp hn] using h

Premises used: Nat.coprime_zero_left, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n u : ℕ
hunit : IsUnit u
refine_2 : IsPrimitiveRoot μ n → ∀ (hcop : u.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ u))
⊢ ∀ (h : IsPrimitiveRoot μ n) (hcop : u.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ u))

Tactic:
_
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n u : ℕ
hunit : IsUnit u
h : IsPrimitiveRoot μ n
refine_2 : u.Coprime n → Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ u))
⊢ ∀ (hcop : u.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ u))

Tactic:
_
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n u : ℕ
hunit : IsUnit u
h : IsPrimitiveRoot μ n
hcop : u.Coprime n
refine_2 : μ = μ ^ u
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ u))

Tactic:
congr
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n u : ℕ
hunit : IsUnit u
h : IsPrimitiveRoot μ n
hcop : u.Coprime n
⊢ μ = μ ^ u

Tactic:
simp [Nat.isUnit_iff.mp hunit]

Premises used: Nat.isUnit_iff, Iff.mp
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
refine_3 :
  a ≠ 0 →
    Prime p →
      (∀ (h : IsPrimitiveRoot μ n) (hcop : a.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ a))) →
        ∀ (h : IsPrimitiveRoot μ n) (hcop : (p * a).Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ (p * a)))
⊢ a ≠ 0 →
    Prime p →
      (∀ (h : IsPrimitiveRoot μ n) (hcop : a.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ a))) →
        ∀ (h : IsPrimitiveRoot μ n) (hcop : (p * a).Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ (p * a)))

Tactic:
_
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
hprime : Prime p
hind : ∀ (h : IsPrimitiveRoot μ n) (hcop : a.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ a))
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
refine_3 : Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ (p * a)))

Tactic:
rw [hind h (Nat.Coprime.coprime_mul_left hcop)]

Premises used: Nat.Coprime.coprime_mul_left
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
m n a p : ℕ
h_1 : a ≠ 0
hprime : Prime p
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
⊢ Nat.Prime p

Tactic:
replace hprime := hprime.nat_prime