-- 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
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

Tactic:
refine ⟨(-1) ^ (m + k) * (∏ j ∈ range k, Z (j + 1)) * ∏ j ∈ Ico k (m + k), (μ ^ (j + 1) - 1),
  ?_, ?_⟩

Result:
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 ℤ {μ}

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

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 (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]

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) ^ #(range k))

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

Tactic:
let n' + 1 := n

Result:
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

Proof state:
case intro.refine_1.hy.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)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ μ ^ (x✝¹ + 1) ∈ adjoin ℤ {μ}

Tactic:
exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton ℤ μ) _

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
k✝ n : ℕ
μ : R
m : ℕ
hn : k✝ < m + k✝ + 1
hμ : IsPrimitiveRoot μ (m + k✝ + 1)
k : ℕ
⊢ ∑ x ∈ range k, μ ^ x ∈ adjoin ℤ {μ}

Tactic:
exact Subalgebra.sum_mem _ fun m _ ↦ Subalgebra.pow_mem _ (self_mem_adjoin_singleton _ μ) _

Result:
no goals

Proof state:
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 ℤ {μ}

Tactic:
refine Subalgebra.prod_mem _ fun _ _ ↦ ?_

Result:
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)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ μ ^ (x✝¹ + 1) - 1 ∈ adjoin ℤ {μ}

Proof state:
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)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ μ ^ (x✝¹ + 1) - 1 ∈ adjoin ℤ {μ}

Tactic:
apply Subalgebra.sub_mem

Result:
case intro.refine_1.hy.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)
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico k (m + k)
⊢ μ ^ (x✝¹ + 1) ∈ adjoin ℤ {μ}

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 ℤ {μ}

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
⊢ ↑m + ↑k + 1 = (((-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]

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
⊢ (-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))