-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem union_left [h : IsCyclotomicExtension T A B] (hS : S ⊆ T) :
    IsCyclotomicExtension S A (adjoin A {b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1})

Proof state:
case h.e'_4
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = ⊤

Tactic:
rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq]

Result:
case h.e'_4
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = adjoin A {a | ∃ a_1 ∈ S, ↑a ^ ↑a_1 = 1}

Proof state:
case refine_1
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑n

Tactic:
obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn)

Result:
case refine_1.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b ↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n

Proof state:
case refine_1.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b ↑n
⊢ ∃ r, IsPrimitiveRoot r ↑n

Tactic:
refine ⟨⟨b, subset_adjoin ⟨n, hn, hb.pow_eq_one⟩⟩, ?_⟩

Result:
case refine_1.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b ↑n
⊢ IsPrimitiveRoot ⟨b, ⋯⟩ ↑n

Proof state:
case refine_1.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b ↑n
⊢ IsPrimitiveRoot ⟨b, ⋯⟩ ↑n

Tactic:
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]

Result:
no goals

Proof state:
case h.e'_4
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = adjoin A {a | ∃ a_1 ∈ S, ↑a ^ ↑a_1 = 1}

Tactic:
norm_cast

Result:
no goals

Proof state:
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
⊢ IsCyclotomicExtension S A ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})

Tactic:
refine ⟨@fun n hn => ?_, fun b => ?_⟩

Result:
case refine_1
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ+
hn : n ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑n

case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ b ∈ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1}

Proof state:
case refine_2
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ b ∈ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1}

Tactic:
convert mem_top (R := A) (x := b)

Result:
case h.e'_4
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = ⊤