-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem of_union_of_dvd (h : ∀ s ∈ S, n ∣ s) (hS : S.Nonempty) [H : IsCyclotomicExtension S A B] :
    IsCyclotomicExtension (S ∪ {n}) A B

Proof state:
case refine_1.inl
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
exact H.exists_prim_root hs

Result:
no goals

Proof state:
case refine_1.inr
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
obtain ⟨m, hm⟩ := hS

Result:
case refine_1.inr.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
m : ℕ+
hm : m ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

Proof state:
case refine_1
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S ∪ {n}
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
rw [mem_union, mem_singleton_iff] at hs

Result:
case refine_1
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S ∨ s = n
⊢ ∃ r, IsPrimitiveRoot r ↑s

Proof state:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
x : B
hx : ∃ n ∈ S, x ^ ↑n = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1

Tactic:
obtain ⟨m, hm⟩ := hx

Result:
case refine_2.intro
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
x : B
m : ℕ+
hm : m ∈ S ∧ x ^ ↑m = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1

Proof state:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ ⊤ ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}

Tactic:
rw [← ((iff_adjoin_eq_top S A B).1 H).2]

Result:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}

Proof state:
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => ?_, ?_⟩

Result:
case refine_1
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S ∪ {n}
⊢ ∃ r, IsPrimitiveRoot r ↑s

case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1} = ⊤

Proof state:
case refine_1
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S ∨ s = n
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
obtain hs | rfl := hs

Result:
case refine_1.inl
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
hs : s ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

case refine_1.inr
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : S.Nonempty
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
⊢ ∃ r, IsPrimitiveRoot r ↑s

Proof state:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
x : B
hx : x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1}
⊢ x ∈ {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}

Tactic:
simp only [union_singleton, mem_insert_iff, mem_setOf_eq] at hx ⊢

Result:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
x : B
hx : ∃ n ∈ S, x ^ ↑n = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1

Proof state:
case h.e'_4
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ ↑s = ↑(s * x) / ↑x

Tactic:
simp only [PNat.mul_coe, Nat.mul_div_left, PNat.pos]

Result:
no goals

Proof state:
case refine_1.inr.intro.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
refine ⟨ζ ^ (x : ℕ), ?_⟩

Result:
case refine_1.inr.intro.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑(s * x)
⊢ IsPrimitiveRoot (ζ ^ ↑x) ↑s

Proof state:
case refine_2.intro
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
x : B
m : ℕ+
hm : m ∈ S ∧ x ^ ↑m = 1
⊢ ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1

Tactic:
exact ⟨m, ⟨Or.inr hm.1, hm.2⟩⟩

Result:
no goals

Proof state:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1} = ⊤

Tactic:
refine _root_.eq_top_iff.2 ?_

Result:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ ⊤ ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}

Proof state:
case refine_1.inr.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
m : ℕ+
hm : m ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
obtain ⟨x, rfl⟩ := h m hm

Result:
case refine_1.inr.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ+
h : ∀ s_1 ∈ S, s ∣ s_1
x : ℕ+
hm : s * x ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

Proof state:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} ≤ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}

Tactic:
refine adjoin_mono fun x hx => ?_

Result:
case refine_2
n : ℕ+
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
h : ∀ s ∈ S, n ∣ s
hS : S.Nonempty
H : IsCyclotomicExtension S A B
x : B
hx : x ∈ {b | ∃ n ∈ S, b ^ ↑n = 1}
⊢ x ∈ {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}