-- Mathlib/RingTheory/RootsOfUnity/Minpoly.lean
theorem separable_minpoly_mod {p : ℕ} [Fact p.Prime] (hdiv : ¬p ∣ n) :
    Separable (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

Proof state:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable

Tactic:
have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 := by
  convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
      (minpoly_dvd_x_pow_sub_one h)
  simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]

Result:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable

Proof state:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
hzero : ↑n = 0
⊢ False

Tactic:
exact hdiv ((ZMod.natCast_zmod_eq_zero_iff_dvd n p).1 hzero)

Result:
no goals

Proof state:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ ↑n ≠ 0

Tactic:
by_contra hzero

Result:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
hzero : ↑n = 0
⊢ False

Proof state:
case h.e'_4
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ X ^ n - 1 = (mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)

Tactic:
simp only [map_sub, map_pow, coe_mapRingHom, map_X, map_one]

Result:
no goals

Proof state:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1

Tactic:
convert RingHom.map_dvd (mapRingHom (Int.castRingHom (ZMod p)))
    (minpoly_dvd_x_pow_sub_one h)

Result:
case h.e'_4
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ X ^ n - 1 = (mapRingHom (Int.castRingHom (ZMod p))) (X ^ n - 1)

Proof state:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ)).Separable

Tactic:
refine Separable.of_dvd (separable_X_pow_sub_C 1 ?_ one_ne_zero) hdvd

Result:
n : ℕ
K : Type u_1
inst✝³ : CommRing K
μ : K
h : IsPrimitiveRoot μ n
inst✝² : IsDomain K
inst✝¹ : CharZero K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1
⊢ ↑n ≠ 0