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
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
⊢ False
have neg₁ : ∀ (hunit : IsUnit (M := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P)), False
Tactic: rcases (squarefree_iff_emultiplicity_le_one (X ^ n - 1)).1 hfree
      (map (Int.castRingHom (ZMod p)) P) with hle | hunit
-- 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)
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
have habs₁ : 1 < emultiplicity (map (Int.castRingHom (ZMod p)) P) (HPow.hPow (α := (ZMod p)[X]) X n - 1)
Tactic: rw [Nat.cast_one] at habs
Cleared hypotheses: habs, hfree, hle
-- 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)
hfree : Squarefree (HPow.hPow (α := (ZMod p)[X]) X n - 1)
hunit : IsUnit (M := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) P)
⊢ False
have hunit₁ : degree (R := ZMod p) (map (Int.castRingHom (ZMod p)) P) = 0
Tactic: replace hunit := degree_eq_zero_of_isUnit hunit
Cleared hypotheses: hunit
-- 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)
hunit : degree (R := ZMod p) (map (Int.castRingHom (ZMod p)) P) = 0
⊢ False
have neg : ∀ (hunit : P.degree = 0), False
Tactic: rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
Cleared hypotheses: hunit
-- 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)
hunit : degree (R := ZMod p) (map (Int.castRingHom (ZMod p)) P) = 0
neg : ∀ (hunit : P.degree = 0), False
⊢ False
have rw : Ne (α := ZMod p) ((Int.castRingHom (ZMod p) : (a : ℤ) → ZMod p) P.leadingCoeff : ZMod p) (0 : ZMod p)
Tactic: rw [degree_map_eq_of_leadingCoeff_ne_zero (Int.castRingHom (ZMod p)) _] at hunit
-- 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: 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]
-- 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: 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]
-- 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))
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
have neg₂ : ∀ (hn : ¬n = 0) (hpos : 0 < n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ p))
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]
-- 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
m : ℕ
hcop : m.Coprime n
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))
have revert : ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : m.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))
Tactic: revert n hcop
Cleared hypotheses: n, h, hcop
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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))
have refine_1 : ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : Nat.Coprime 0 n),
  Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (HPow.hPow (β := ℕ) μ 0))
Tactic: refine UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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))
⊢ ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : m.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))
have refine_2 : ∀ {n : ℕ} (x : ℕ),
  IsUnit x → ∀ (h : IsPrimitiveRoot μ n) (hcop : x.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ x))
Tactic: refine UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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))
⊢ ∀ {n : ℕ} (h : IsPrimitiveRoot μ n) (hcop : m.Coprime n), Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ m))
have 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)))
Tactic: refine UniqueFactorizationMonoid.induction_on_prime m ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (HPow.hPow (β := ℕ) μ 0))
have refine_1 : μ = HPow.hPow (β := ℕ) μ 0
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ u))
have refine_2 : μ = μ ^ u
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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
⊢ Eq (α := ℤ[X]) (minpoly ℤ μ) (minpoly ℤ (μ ^ (p * a)))
have refine_3 : Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))
Tactic: rw [hind h (Nat.Coprime.coprime_mul_left hcop)]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
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
⊢ Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))
have hprime₁ : Nat.Prime p
Tactic: replace hprime := hprime.nat_prime
Cleared hypotheses: hprime
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
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
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
⊢ Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))
have hdiv : ¬p ∣ n
Tactic: have hdiv := (Nat.Prime.coprime_iff_not_dvd hprime).1 (Nat.Coprime.coprime_mul_right hcop)
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (hypothesis)
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
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
⊢ Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))
have this : Fact (Nat.Prime p)
Tactic: haveI := Fact.mk hprime
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
this : Fact (Nat.Prime p)
⊢ Eq (α := ℤ[X]) (minpoly ℤ (μ ^ a)) (minpoly ℤ (μ ^ (p * a)))
have refine_3 : Eq (α := ℤ[X]) (minpoly ℤ ((μ ^ a) ^ p)) (minpoly ℤ (μ ^ (p * a)))
Tactic: rw [minpoly_eq_pow (h.pow_of_coprime a (Nat.Coprime.coprime_mul_left hcop)) hdiv]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
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
h : IsPrimitiveRoot μ n
hcop : (p * a).Coprime n
hprime : Nat.Prime p
hdiv : ¬p ∣ n
this : Fact (Nat.Prime p)
⊢ Eq (α := ℤ[X]) (minpoly ℤ ((μ ^ a) ^ p)) (minpoly ℤ (μ ^ (p * a)))
have refine_3 : (μ ^ a) ^ p = μ ^ (p * a)
Tactic: congr 1
-- 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
m : ℕ
hcop : m.Coprime n
⊢ IsRoot (map (Int.castRingHom K) (minpoly ℤ μ)) (μ ^ m)
have simp : eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0
Tactic: simp only [minpoly_eq_pow_coprime h hcop, IsRoot.def, eval_map]
-- 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
inst_3 : DecidableEq K
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
have pos : ∀ (hn : n = 0), primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
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
inst_3 : DecidableEq K
pos : ∀ (hn : n = 0), primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
have neg : ∀ (hn : ¬n = 0), primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
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
inst_3 : DecidableEq K
hn : ¬n = 0
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
have this : NeZero n
Tactic: have : NeZero n := ⟨hn⟩
-- 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
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
⊢ primitiveRoots n K ⊆ Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))
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
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
x : K
hx : x ∈ primitiveRoots n K
⊢ Membership.mem (γ := Finset K) (Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))) x
have neg : ∀ m < n,
  ∀ (hcop : m.Coprime n) (hx : μ ^ m ∈ primitiveRoots n K),
    Membership.mem (γ := Finset K) (Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))) (μ ^ m)
Tactic: obtain ⟨m, _, hcop, rfl⟩ := (isPrimitiveRoot_iff h).1 ((mem_primitiveRoots hpos).1 hx)
Cleared hypotheses: x, hx
-- 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
inst_3 : DecidableEq K
hn : ¬n = 0
this : NeZero n
hpos : 0 < n
m : ℕ
left : m < n
hcop : m.Coprime n
hx : μ ^ m ∈ primitiveRoots n K
⊢ Membership.mem (γ := Finset K) (Multiset.toFinset (roots (map (Int.castRingHom K) (minpoly ℤ μ)))) (μ ^ m)
have neg : Membership.mem (γ := Multiset K) (roots (map (Int.castRingHom K) (minpoly ℤ μ))) (μ ^ m)
Tactic: simp only [Multiset.mem_toFinset]