-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic {n : ℕ+} [IsDomain B] {ζ : B}
    (hζ : IsPrimitiveRoot ζ n) : adjoin A ((cyclotomic n A).rootSet B) = adjoin A {ζ}

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

Tactic:
simpa only [hx, mem_rootSet', map_cyclotomic, aeval_def, ← eval_map, IsRoot] using
  And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic n.pos)

Result:
no goals

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

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

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

case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ {ζ}
⊢ x ∈ (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
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ x ∈ ↑(adjoin A {ζ})

Tactic:
suffices hx : x ^ n.1 = 1 by
  obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
  exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)

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

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

Tactic:
exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)

Result:
no goals

Proof state:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ ∃ 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
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ (cyclotomic (↑n) B).IsRoot x

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

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

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

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

Tactic:
refine (isRoot_of_unity_iff n.pos B).2 ?_

Result:
case refine_1
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ ∃ 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
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : cyclotomic (↑n) B ≠ 0 ∧ (cyclotomic (↑n) B).IsRoot x
⊢ (cyclotomic (↑n) B).IsRoot x

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
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ (cyclotomic (↑n) A).rootSet B
⊢ (cyclotomic (↑n) B).IsRoot x

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

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

Proof state:
case refine_2
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x ∈ {ζ}
⊢ x ∈ (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
n : ℕ+
inst✝ : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ ↑n
x : B
hx : x = ζ
⊢ x ∈ (cyclotomic (↑n) A).rootSet B