awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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_1 : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k))
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (HPow.hPow (α := R) (-1) (m + k) * ∏ j ∈ range k, Z (j + 1))
have refine_1₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ range k, Z (j + 1))
Tactic: apply Subalgebra.mul_mem
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1))
have refine_1 : ∀ x ∈ Ico k (m + k), Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1) - 1)
Tactic: refine Subalgebra.prod_mem _ fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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)
x : ℕ
h : x ∈ Ico k (m + k)
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1) - 1)
have refine_1 : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1))
Tactic: apply Subalgebra.sub_mem
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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)
x : ℕ
h : x ∈ Ico k (m + k)
refine_1 : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1))
⊢ Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] (μ ^ (x + 1) - 1)
have refine_1₁ : Membership.mem (γ := Subalgebra ℤ R) ℤ[μ] 1
Tactic: apply Subalgebra.sub_mem
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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)
⊢ (↑(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
have 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
Tactic: push_cast
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (hypothesis)
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)
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
⊢ 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
have 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))
Tactic: rw [← this, mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
⊢ 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))
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
| ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)
have enter : (μ - 1) ^ k
Tactic: enter [2, 2, 2]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
| (μ - 1) ^ k
have rw : (μ - 1) ^ #(range k)
Tactic: rw [← card_range k]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
| ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)
have enter : (μ - 1) ^ #(range k)
Tactic: enter [2, 2, 2]; rw [← card_range k]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)
have 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))
Tactic: conv => enter [2, 2, 2]; rw [← card_range k]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ #(range k))
have 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))
Tactic: rw [← prod_range_mul_prod_Ico _ (Nat.le_add_left k m), mul_comm _ (_ ^ #_), ← mul_assoc,
      prod_mul_pow_card]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
| 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))
have h : ∀ (j : ℕ), Z (j + 1) * (μ - 1)
Tactic: enter [2, 1, 2, j]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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 : ℕ
| Z (j + 1) * (μ - 1)
have h : μ ^ (j + 1) - 1
Tactic: rw [← (Zdef _).2]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
| 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))
have h : ∀ (j : ℕ), μ ^ (j + 1) - 1
Tactic: enter [2, 1, 2, j]; rw [← (Zdef _).2]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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
⊢ 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))
have 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))
Tactic: conv => enter [2, 1, 2, j]; rw [← (Zdef _).2]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Lemmas (goal)
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))
⊢ 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))
have 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))
Tactic: conv => enter [2, 1, 2, j]; rw [← (Zdef _).2]
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ IsIntegral ℤ μ
have h₁ : (HPow.hPow (α := ℤ[X]) X n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0
Tactic: use X ^ n - 1
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
⊢ (HPow.hPow (α := ℤ[X]) X n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0
have h₁ : (HPow.hPow (α := ℤ[X]) X n - 1).Monic
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.RootsOfUnity.Minpoly (goal)
Goal:
n : ℕ
K : Type u_1
inst : CommRing K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
h₁ : (HPow.hPow (α := ℤ[X]) X n - 1).Monic
⊢ (HPow.hPow (α := ℤ[X]) X n - 1).Monic ∧ eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0
have h₂ : eval₂ (algebraMap ℤ K) μ (HPow.hPow (α := ℤ[X]) X n - 1) = 0
Tactic: constructor
-- 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
⊢ minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1
have inl : ∀ (h : IsPrimitiveRoot μ 0), minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1
Tactic: rcases n.eq_zero_or_pos with (rfl | h0)
Cleared hypotheses: n, h
-- 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
inl : ∀ (h : IsPrimitiveRoot μ 0), minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) (β := ℕ) X 0 - 1
⊢ minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1
have inr : ∀ (h0 : n > 0), minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1
Tactic: rcases n.eq_zero_or_pos with (rfl | h0)
-- 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
h0 : n > 0
⊢ minpoly ℤ μ ∣ HPow.hPow (α := ℤ[X]) X n - 1
have inr : Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) (HPow.hPow (α := ℤ[X]) X n - 1) : K) (0 : K)
Tactic: apply minpoly.isIntegrallyClosed_dvd (isIntegral h h0)
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ map (Int.castRingHom (ZMod p)) (minpoly ℤ μ) ∣ HPow.hPow (α := (ZMod p)[X]) X n - 1
have 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)
Tactic: convert! _root_.map_dvd (mapRingHom (Int.castRingHom (ZMod p))) (minpoly_dvd_x_pow_sub_one h)
-- 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 : ℕ
inst_3 : Fact (Nat.Prime p)
hdiv : ¬p ∣ n
⊢ Separable (R := ZMod p) (map (Int.castRingHom (ZMod p)) (minpoly ℤ μ))
have hdvd : 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]
-- 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 : ℕ
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 ℤ μ))
have refine : Ne (α := ZMod p) (↑n : ZMod p) 0
Tactic: refine Separable.of_dvd (separable_X_pow_sub_C 1 ?_ one_ne_zero) hdvd
-- 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 : ℕ
hdiv : ¬p ∣ n
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
have inl : ∀ (h : IsPrimitiveRoot μ 0) (hdiv : ¬p ∣ 0),
  Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
Cleared hypotheses: n, h, hdiv
-- 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 : ℕ
hdiv : ¬p ∣ n
inl :
  ∀ (h : IsPrimitiveRoot μ 0) (hdiv : ¬p ∣ 0),
    Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
have inr : ∀ (hpos : n > 0), Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
Tactic: rcases n.eq_zero_or_pos with (rfl | hpos)
-- 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 : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := ⋯
⊢ Dvd.dvd (α := ℤ[X]) (minpoly ℤ μ) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)))
have inr : Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)) : ℤ[X]) : K)
  (0 : K)
Tactic: refine minpoly.isIntegrallyClosed_dvd (h.isIntegral hpos) ?_
-- 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 : ℕ
hdiv : ¬p ∣ n
hpos : n > 0
this : IsIntegrallyClosed ℤ := ⋯
⊢ Eq (α := K) ((Polynomial.aeval μ : (a : ℤ[X]) → K) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) (minpoly ℤ (μ ^ p)) : ℤ[X]) : K)
    (0 : K)
have inr : Eq (α := K) ((Polynomial.aeval (μ ^ p) : (a : ℤ[X]) → K) (minpoly ℤ (μ ^ p)) : 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]
-- 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
Q : ℤ[X] := minpoly ℤ (μ ^ p)
⊢ HPow.hPow (α := (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) p =
    map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q)
have rw : Eq (α := (ZMod p)[X])
  ((expand (ZMod p) p : (a : (ZMod p)[X]) → (ZMod p)[X]) (map (Int.castRingHom (ZMod p)) Q) : (ZMod p)[X])
  (map (Int.castRingHom (ZMod p)) ((expand ℤ p : (a : ℤ[X]) → ℤ[X]) Q) : (ZMod p)[X])
Tactic: rw [← ZMod.expand_card, map_expand]