awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
refine_2 :
  HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1 =
    ((HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) *
      (μ - 1) ^ k
⊢ (↑(m + k + 1) : R) =
    ((HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) *
      (μ - 1) ^ k

Tactic:
push_cast
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1

Tactic:
have := Nat.cast_add (R := R) m k ▸ hμ.prod_pow_sub_one_eq_order
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
refine_2 :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    HPow.hPow (α := R) (-1) (m + k) *
      ((∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k))
⊢ HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1 =
    ((HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) *
      (μ - 1) ^ k

Tactic:
rw [← this, mul_assoc, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
refine_2 :
  ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)
⊢ HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    HPow.hPow (α := R) (-1) (m + k) *
      ((∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
enter : (μ - 1) ^ k
| ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Tactic:
enter [2, 2, 2]
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
rw : (μ - 1) ^ #(range k)
| (μ - 1) ^ k

Tactic:
rw [← card_range k]

Premises used: Finset.card_range
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
enter : (μ - 1) ^ #(range k)
| ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Tactic:
enter [2, 2, 2]; rw [← card_range k]

Premises used: Finset.card_range
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
refine_2 :
  ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ #(range k))
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Tactic:
conv => enter [2, 2, 2]; rw [← card_range k]

Premises used: Finset.card_range
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
refine_2 :
  HMul.hMul (α := R) (∏ k ∈ range k, (μ ^ (k + 1) - 1)) (∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1)) =
    HMul.hMul (α := R) (∏ a ∈ range k, Z (a + 1) * (μ - 1)) (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ #(range k))

Tactic:
rw [← prod_range_mul_prod_Ico _ (Nat.le_add_left k m), mul_comm _ (_ ^ #_), ← mul_assoc,
      prod_mul_pow_card]

Premises used: Finset.prod_range_mul_prod_Ico, Finset.prod_mul_pow_card, mul_assoc, Nat.le_add_left, HPow.hPow, mul_comm, Finset.card
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
h : ∀ (j : ℕ), Z (j + 1) * (μ - 1)
| HMul.hMul (α := R) (∏ k ∈ range k, (μ ^ (k + 1) - 1)) (∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1)) =
    HMul.hMul (α := R) (∏ a ∈ range k, Z (a + 1) * (μ - 1)) (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))

Tactic:
enter [2, 1, 2, j]
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
j : ℕ
h : μ ^ (j + 1) - 1
| Z (j + 1) * (μ - 1)

Tactic:
rw [← (Zdef _).2]

Premises used: And.right
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
h : ∀ (j : ℕ), μ ^ (j + 1) - 1
| HMul.hMul (α := R) (∏ k ∈ range k, (μ ^ (k + 1) - 1)) (∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1)) =
    HMul.hMul (α := R) (∏ a ∈ range k, Z (a + 1) * (μ - 1)) (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))

Tactic:
enter [2, 1, 2, j]; rw [← (Zdef _).2]

Premises used: And.right
-- Module: Mathlib.RingTheory.RootsOfUnity.Lemmas
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ (z : R), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] z ∧ μ ^ k - 1 = z * (μ - 1)
Z : (k : ℕ) → R :=
  fun (k : ℕ) ↦
    Classical.choose (p := fun (x : R) ↦ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] x ∧ μ ^ k - 1 = x * (μ - 1)) ⋯
Zdef : ∀ (k : ℕ), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (Z k) ∧ μ ^ k - 1 = Z k * (μ - 1)
this :
  HPow.hPow (α := R) (-1) (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = HAdd.hAdd (α := R) (↑m : R) (↑k : R) + 1
conv :
  HMul.hMul (α := R) (∏ k ∈ range k, (μ ^ (k + 1) - 1)) (∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1)) =
    HMul.hMul (α := R) (∏ a ∈ range k, Z (a + 1) * (μ - 1)) (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))
refine_2 :
  HMul.hMul (α := R) (∏ k ∈ range k, (μ ^ (k + 1) - 1)) (∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1)) =
    HMul.hMul (α := R) (∏ j ∈ range k, (μ ^ (j + 1) - 1)) (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))
⊢ HMul.hMul (α := R) (∏ k ∈ range k, (μ ^ (k + 1) - 1)) (∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1)) =
    HMul.hMul (α := R) (∏ a ∈ range k, Z (a + 1) * (μ - 1)) (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))

Tactic:
conv => enter [2, 1, 2, j]; rw [← (Zdef _).2]

Premises used: And.right
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
h₁ : (HPow.hPow (α := ℤ[X]) X n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0
⊢ IsIntegral ℤ μ

Tactic:
use X ^ n - 1

Premises used: Polynomial.X
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
h₁ : (HPow.hPow (α := ℤ[X]) X n - 1).Monic
h₂ : eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0
⊢ (HPow.hPow (α := ℤ[X]) X n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0

Tactic:
constructor
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (HPow.hPow (α := ℤ[X]) X n - 1).Monic

Tactic:
monic_X_pow_sub_C 1 (ne_of_lt hpos).symm

Premises used: Polynomial.monic_X_pow_sub_C, Ne.symm, OfNat.ofNat, ne_of_lt
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (HPow.hPow (α := ℤ[X]) X n - 1).Monic

Tactic:
exact monic_X_pow_sub_C 1 (ne_of_lt hpos).symm

Premises used: Polynomial.monic_X_pow_sub_C, Ne.symm, OfNat.ofNat, ne_of_lt
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0

Tactic:
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, eval₂_one, eval₂_X_pow, eval₂_sub,
      sub_self]

Premises used: Polynomial.eval₂_X_pow, Polynomial.eval₂_one, sub_self, IsPrimitiveRoot.iff_def, Polynomial.eval₂_sub, And.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
inl : ∀ (h : IsPrimitiveRoot μ 0), minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1
inr : ∀ (h0 : n > 0), minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1
⊢ minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
rcases n.eq_zero_or_pos with (rfl | h0)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
h : IsPrimitiveRoot μ 0
⊢ minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1

Tactic:
simp
-- 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
h0 : n > 0
inr : Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) (HPow.hPow (α := ℤ[X]) X n - 1) : K) (0 : K)
⊢ minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1

Tactic:
apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)

Premises used: IsPrimitiveRoot.isIntegral, minpoly.isIntegrallyClosed_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
h0 : n > 0
⊢ Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) (HPow.hPow (α := ℤ[X]) X n - 1) : K) (0 : K)

Tactic:
simp only [((IsPrimitiveRoot.iff_def μ n).mp h).left, aeval_X_pow,
    aeval_one, map_sub, sub_self]

Premises used: map_sub, sub_self, Polynomial.aeval_X_pow, IsPrimitiveRoot.iff_def, Polynomial.aeval_one, And.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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Dvd.dvd (α := (ZMod p)[X])
    ((mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (minpoly ℤ μ) : (ZMod p)[X])
    ((mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (HPow.hPow (α := ℤ[X]) X n - 1) : (ZMod p)[X])

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

Premises used: ZMod, map_dvd, Int.castRingHom, Polynomial.mapRingHom, 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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
h₁ :
  HPow.hPow (α := (ZMod p)[X]) X n - 1 =
    (mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (HPow.hPow (α := ℤ[X]) X n - 1)
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1

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

Premises used: ZMod, map_dvd, Int.castRingHom, Polynomial.mapRingHom, 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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ HPow.hPow (α := (ZMod p)[X]) X n - 1 =
    (mapRingHom (Int.castRingHom (ZMod p)) : (a : ℤ[X]) → (ZMod p)[X]) (HPow.hPow (α := ℤ[X]) X n - 1)

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

Premises used: map_sub, Polynomial.map_X, map_pow, Polynomial.coe_mapRingHom, map_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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1

Tactic:
have hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ X ^ n - 1 := by
    convert! _root_.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]
-- 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
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
⊢ Separable (R := ZMod p) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

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

Premises used: Polynomial.separable_X_pow_sub_C, one_ne_zero, OfNat.ofNat, Polynomial.Separable.of_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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
refine : Ne (α := ZMod p) (↑n : ZMod p) 0
⊢ Separable (R := ZMod p) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

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

Premises used: Polynomial.separable_X_pow_sub_C, one_ne_zero, OfNat.ofNat, Polynomial.Separable.of_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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
by_contra : ∀ (hzero : Eq (α := ZMod p) (↑n : ZMod p) 0), False
⊢ Ne (α := ZMod p) (↑n : ZMod p) 0

Tactic:
by_contra hzero
-- 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
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hzero : Eq (α := ZMod p) (↑n : ZMod p) 0
⊢ False

Tactic:
hdiv ((ZMod.natCast_eq_zero_iff n p).1 hzero)

Premises used: ZMod.natCast_eq_zero_iff, 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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
hdvd : map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
hzero : Eq (α := ZMod p) (↑n : ZMod p) 0
⊢ False

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

Premises used: ZMod.natCast_eq_zero_iff, 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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Squarefree (R := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))

Tactic:
(separable_minpoly_mod h hdiv).squarefree

Premises used: IsPrimitiveRoot.separable_minpoly_mod, Polynomial.Separable.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 : ℕ
hdiv : ¬p ∣ n
inl :
  ∀ (h : IsPrimitiveRoot μ 0) (hdiv : ¬p ∣ 0),
    Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
inr : ∀ (hpos : n > 0), Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))

Tactic:
rcases n.eq_zero_or_pos with (rfl | hpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.RootsOfUnity.Minpoly
Goal:
K : Type u_1
inst : CommRing K
μ : K
inst_1 : IsDomain K
inst_2 : CharZero K
p : ℕ
h : IsPrimitiveRoot μ 0
hdiv : ¬p ∣ 0
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (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 : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := ⋯
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))

Tactic:
minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) ?_

Premises used: IsPrimitiveRoot.isIntegral, minpoly.isIntegrallyClosed_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 : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := ⋯
inr :
  Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)) : ℤ[X]) : K)
    (0 : K)
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))

Tactic:
refine minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) ?_

Premises used: IsPrimitiveRoot.isIntegral, minpoly.isIntegrallyClosed_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 : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := ⋯
inr : Eq (α := K) ((Polynomial.aeval (μ ^ p) : (a : ℤ[X]) → K) (minpoly ℤ (μ ^ p)) : K) (0 : K)
⊢ Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)) : ℤ[X]) : K)
    (0 : K)

Tactic:
rw [aeval_def, coe_expand, ← comp, eval₂_eq_eval_map, map_comp, Polynomial.map_pow, map_X,
    eval_comp, eval_X_pow, ← eval₂_eq_eval_map, ← aeval_def]

Premises used: Polynomial.eval_X_pow, Polynomial.map_pow, Polynomial.map_X, Polynomial.aeval_def, Polynomial.eval_comp, Polynomial.coe_expand, Polynomial.map_comp, Polynomial.comp, Polynomial.eval₂_eq_eval_map
-- 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:
minpoly.aeval _ _

Premises used: minpoly.aeval