-- 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))
neg neg₁ : ∀ (hn : ¬n = 0), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
neg₂ : ∀ (hn : ¬n = 0) (hpos : 0 < n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
neg₃ : ∀ (hn : ¬n = 0) (hpos : 0 < n) (hdiff : ¬Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))), False
neg₄ :
  ∀ (hn : ¬n = 0) (hpos : 0 < n),
    let P : ℤ[X] := minpoly ℤ μ;
    ∀ (hdiff : ¬P = minpoly ℤ (μ ^ p)), False
neg₅ :
  ∀ (hn : ¬n = 0) (hpos : 0 < n),
    let P : ℤ[X] := minpoly ℤ μ;
    let Q : ℤ[X] := minpoly ℤ (μ ^ p);
    ∀ (hdiff : ¬P = Q), False
neg₆ :
  ∀ (hn : ¬n = 0) (hpos : 0 < n),
    let P : ℤ[X] := minpoly ℤ μ;
    let Q : ℤ[X] := minpoly ℤ (μ ^ p);
    ∀ (hdiff : ¬P = Q) (Pmonic : P.Monic), False
neg₇ :
  ∀ (hn : ¬n = 0) (hpos : 0 < n),
    let P : ℤ[X] := minpoly ℤ μ;
    let Q : ℤ[X] := minpoly ℤ (μ ^ p);
    ∀ (hdiff : ¬P = Q) (Pmonic : P.Monic) (Qmonic : Q.Monic), False
neg₈ :
  ∀ (hn : ¬n = 0) (hpos : 0 < n),
    let P : ℤ[X] := minpoly ℤ μ;
    let Q : ℤ[X] := minpoly ℤ (μ ^ p);
    ∀ (hdiff : ¬P = Q) (Pmonic : P.Monic) (Qmonic : Q.Monic) (Pirr : Irreducible P), False
neg₉ :
  ∀ (hn : ¬n = 0) (hpos : 0 < n),
    let P : ℤ[X] := minpoly ℤ μ;
    let Q : ℤ[X] := minpoly ℤ (μ ^ p);
    ∀ (hdiff : ¬P = Q) (Pmonic : P.Monic) (Qmonic : Q.Monic) (Pirr : Irreducible P) (Qirr : Irreducible Q), False
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
have neg₁₀ : ∀ (hn : ¬n = 0) (hpos : 0 < n),
  let P : ℤ[X] := minpoly ℤ μ;
  let Q : ℤ[X] := minpoly ℤ (μ ^ p);
  ∀ (hdiff : ¬P = Q) (Pmonic : P.Monic) (Qmonic : Q.Monic) (Pirr : Irreducible P) (Qirr : Irreducible Q)
    (PQprim : (P * Q).IsPrimitive), False
Tactic: classical
  by_cases hn : n = 0
  · simp_all
  have hpos := Nat.pos_of_ne_zero hn
  by_contra hdiff
  set P := minpoly ℤ μ
  set Q := minpoly ℤ (μ ^ p)
  have Pmonic : P.Monic := minpoly.monic (h.isIntegral hpos)
  have Qmonic : Q.Monic := minpoly.monic ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
  have Pirr : Irreducible P := minpoly.irreducible (h.isIntegral hpos)
  have Qirr : Irreducible Q := minpoly.irreducible ((h.pow_of_prime hprime.1 hdiv).isIntegral hpos)
  have PQprim : IsPrimitive (P * Q) := Pmonic.isPrimitive.mul Qmonic.isPrimitive
  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)
  replace prod := _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) prod
  rw [coe_mapRingHom, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_one,
    Polynomial.map_pow, map_X] at prod
  obtain ⟨R, hR⟩ := minpoly_dvd_mod_p h hdiv
  rw [hR, ← mul_assoc, ← Polynomial.map_mul, ← sq, Polynomial.map_pow] at prod
  have habs : map (Int.castRingHom (ZMod p)) P ^ 2 ∣ map (Int.castRingHom (ZMod p)) P ^ 2 * R := by
    use R
  replace habs :=
    lt_of_lt_of_le (Nat.cast_lt.2 one_lt_two)
      (le_emultiplicity_of_pow_dvd (dvd_trans habs prod))
  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
  rcases (squarefree_iff_emultiplicity_le_one (X ^ n - 1)).1 hfree
      (map (Int.castRingHom (ZMod p)) P) with hle | hunit
  · rw [Nat.cast_one] at habs; exact hle.not_gt habs
  · replace hunit := degree_eq_zero_of_isUnit hunit
    rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
    · exact (minpoly.degree_pos (isIntegral h hpos)).ne' hunit
    simp only [Pmonic, eq_intCast, Monic.leadingCoeff, Int.cast_one, Ne, not_false_iff,
      one_ne_zero]