-- Mathlib/RingTheory/RootsOfUnity/Lemmas.lean
/-- If `μ` is a primitive `n`th root of unity in `R` and `k < n`, then `n` is divisible
by `(μ-1)^k` in `ℤ[μ] ⊆ R`. -/
lemma self_sub_one_pow_dvd_order {k n : ℕ} (hn : k < n) {μ : R} (hμ : IsPrimitiveRoot μ n) :
    ∃ z ∈ adjoin ℤ {μ}, n = z * (μ - 1) ^ k

Proof state:
case intro.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ↑m + ↑k + 1 = (((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k

Tactic:
have := Nat.cast_add (R := R) m k ▸ hμ.prod_pow_sub_one_eq_order

Result:
case intro.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ ↑m + ↑k + 1 = (((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
⊢ ∃ z ∈ adjoin ℤ {μ}, ↑(m + k + 1) = z * (μ - 1) ^ k

Tactic:
have Zdef k : Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1) :=
  Classical.choose_spec <| hdvd k

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∃ z ∈ adjoin ℤ {μ}, ↑(m + k + 1) = z * (μ - 1) ^ k

Proof state:
case intro.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (-1) ^ (m + k) * ((∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k))

Tactic:
congr 1

Result:
case intro.refine_2.e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) =
    (∏ j ∈ range k, Z (j + 1)) * ((∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1)) * (μ - 1) ^ k)

Proof state:
case intro.refine_1.hy.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ 1 ∈ adjoin ℤ {μ}

Tactic:
exact Subalgebra.one_mem _

Result:
no goals

Proof state:
case intro.refine_2.e_a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
this : (-1) ^ (m + k) * ∏ k ∈ range (m + k), (μ ^ (k + 1) - 1) = ↑m + ↑k + 1
⊢ (∏ k ∈ range k, (μ ^ (k + 1) - 1)) * ∏ k ∈ Ico k (m + k), (μ ^ (k + 1) - 1) =
    (∏ 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]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
n' : ℕ
hn : k < n' + 1
hμ : IsPrimitiveRoot μ (n' + 1)
⊢ ∃ z ∈ adjoin ℤ {μ}, ↑(n' + 1) = z * (μ - 1) ^ k

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.le_of_lt_succ hn)

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
⊢ ∃ z ∈ adjoin ℤ {μ}, ↑(m + k + 1) = z * (μ - 1) ^ k

Proof state:
case intro.refine_1
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ((-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ adjoin ℤ {μ}

Tactic:
apply Subalgebra.mul_mem

Result:
case intro.refine_1.hx
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ (-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1) ∈ adjoin ℤ {μ}

case intro.refine_1.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1) ∈ adjoin ℤ {μ}

Proof state:
case intro.refine_1.hx
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ (-1) ^ (m + k) * ∏ j ∈ range k, Z (j + 1) ∈ adjoin ℤ {μ}

Tactic:
apply Subalgebra.mul_mem

Result:
case intro.refine_1.hx.hx
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ (-1) ^ (m + k) ∈ adjoin ℤ {μ}

case intro.refine_1.hx.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ range k, Z (j + 1) ∈ adjoin ℤ {μ}

Proof state:
case intro.refine_1.hx.hy
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k n : ℕ
μ : R
m : ℕ
hn : k < m + k + 1
hμ : IsPrimitiveRoot μ (m + k + 1)
hdvd : ∀ (k : ℕ), ∃ z ∈ adjoin ℤ {μ}, μ ^ k - 1 = z * (μ - 1)
Z : ℕ → R := fun k => Classical.choose ⋯
Zdef : ∀ (k : ℕ), Z k ∈ adjoin ℤ {μ} ∧ μ ^ k - 1 = Z k * (μ - 1)
⊢ ∏ j ∈ range k, Z (j + 1) ∈ adjoin ℤ {μ}

Tactic:
exact Subalgebra.prod_mem _ fun _ _ ↦ (Zdef _).1

Result:
no goals