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

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

Tactic:
refine ⟨fun hn => ((isCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => ?_⟩

Result:
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
this : {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} = {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}
b : B
⊢ b ∈ adjoin ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1}) {b | ∃ n ∈ T, 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 (S ∪ T) A B
⊢ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1} ≤ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
rintro x (⟨n, hn⟩ | ⟨n, hn⟩)

Result:
case refine_2.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hn : n ∈ S ∧ x ^ ↑n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

case refine_2.inr.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hn : n ∈ T ∧ x ^ ↑n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

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

Tactic:
replace h := ((isCyclotomicExtension_iff _ _ _).1 h).2 b

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

Proof state:
case refine_1.intro.intro.inr
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

Tactic:
right

Result:
case refine_1.intro.intro.inr.h
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ T, b ^ ↑n = 1}

Proof state:
case refine_2.inl.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hn : n ∈ S ∧ x ^ ↑n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
exact ⟨n, Or.inl hn.1, hn.2⟩

Result:
no goals

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 (S ∪ T) A B
⊢ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} ≤ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

Tactic:
rintro x ⟨n, hn₁ | hn₂, hnpow⟩

Result:
case refine_1.intro.intro.inl
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

case refine_1.intro.intro.inr
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

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

Tactic:
rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h

Result:
no goals

Proof state:
case refine_2.inr.intro
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hn : n ∈ T ∧ x ^ ↑n = 1
⊢ x ∈ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}

Tactic:
exact ⟨n, Or.inr hn.1, hn.2⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.inr.h
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₂ : n ∈ T
⊢ x ∈ {b | ∃ n ∈ T, b ^ ↑n = 1}

Tactic:
exact ⟨n, hn₂, hnpow⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.inl
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

Tactic:
left

Result:
case refine_1.intro.intro.inl.h
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1}

Proof state:
case refine_1.intro.intro.inl.h
S T : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ+
hnpow : x ^ ↑n = 1
hn₁ : n ∈ S
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1}

Tactic:
exact ⟨n, hn₁, hnpow⟩

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 (S ∪ T) A B
⊢ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} = {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

Tactic:
refine le_antisymm ?_ ?_

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 (S ∪ T) A B
⊢ {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} ≤ {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}

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