-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem adjoin_roots_cyclotomic_eq_adjoin_nth_roots [IsDomain B] {ζ : B} {n : ℕ+}
    (hζ : IsPrimitiveRoot ζ n) :
    adjoin A ((cyclotomic n A).rootSet B) =
      adjoin A {b : B | ∃ a : ℕ+, a ∈ ({n} : Set ℕ+) ∧ b ^ (a : ℕ) = 1}

Proof state:
case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ^ ↑n = 1
⊢ x ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))

Tactic:
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx

Result:
case refine_2.intro.intro
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ^ i ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))

Proof state:
case refine_2.intro.intro
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ cyclotomic (↑n) B ≠ 0 ∧ (cyclotomic (↑n) B).IsRoot ζ

Tactic:
exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic n.pos⟩

Result:
no goals

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ ∃ i ∈ (↑n).divisors, (cyclotomic i B).IsRoot x

Tactic:
refine ⟨n, Nat.mem_divisors_self n n.ne_zero, ?_⟩

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ (cyclotomic (↑n) B).IsRoot x

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A ((cyclotomic (↑n) A).rootSet B) = adjoin A {b | b ^ ↑n = 1}

Tactic:
refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ x ∈ {b | b ^ ↑n = 1}

case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ {b | b ^ ↑n = 1}
⊢ x ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ (cyclotomic (↑n) B).IsRoot x

Tactic:
rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map, ← aeval_def]

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ (aeval x) (cyclotomic (↑n) A) = 0

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ x ^ ↑n = 1

Tactic:
rw [isRoot_of_unity_iff n.pos]

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ ∃ i ∈ (↑n).divisors, (cyclotomic i B).IsRoot x

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ (aeval x) (cyclotomic (↑n) A) = 0

Tactic:
exact hx.2

Result:
no goals

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ x ∈ {b | b ^ ↑n = 1}

Tactic:
rw [mem_rootSet'] at hx

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ x ∈ {b | b ^ ↑n = 1}

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ x ∈ {b | b ^ ↑n = 1}

Tactic:
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq]

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : map (algebraMap A B) (cyclotomic (↑n) A) ≠ 0 ∧ (aeval x) (cyclotomic (↑n) A) = 0
⊢ x ^ ↑n = 1

Proof state:
case refine_2.intro.intro
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ^ i ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))

Tactic:
refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)

Result:
case refine_2.intro.intro
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ∈ (cyclotomic (↑n) A).rootSet B

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A ((cyclotomic (↑n) A).rootSet B) = adjoin A {b | ∃ a ∈ {n}, b ^ ↑a = 1}

Tactic:
simp only [mem_singleton_iff, exists_eq_left, map_cyclotomic]

Result:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin A ((cyclotomic (↑n) A).rootSet B) = adjoin A {b | b ^ ↑n = 1}

Proof state:
case refine_2.intro.intro
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ ζ ∈ (cyclotomic (↑n) A).rootSet B

Tactic:
rw [mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, map_cyclotomic, ← IsRoot]

Result:
case refine_2.intro.intro
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
i : ℕ
left✝ : i < ↑n
hx : (ζ ^ i) ^ ↑n = 1
⊢ cyclotomic (↑n) B ≠ 0 ∧ (cyclotomic (↑n) B).IsRoot ζ

Proof state:
case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ {b | b ^ ↑n = 1}
⊢ x ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))

Tactic:
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hx

Result:
case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
ζ : B
n : ℕ+
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ^ ↑n = 1
⊢ x ∈ ↑(adjoin A ((cyclotomic (↑n) A).rootSet B))