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

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

Tactic:
obtain ⟨y, hy⟩ := hS

Result:
case refine_2.intro.intro.inl.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ s ∈ S, m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
y : ℕ+
hy : y ∈ S
⊢ ∃ n ∈ S, x ^ ↑n = 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 ∪ {n}) A B
s : ℕ+
hs : s ∈ S
⊢ ∃ r, IsPrimitiveRoot r ↑s

Tactic:
exact H.exists_prim_root (subset_union_left hs)

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 ∪ {n}) A B
x : B
hx : x ∈ {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 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 ∪ {n}) A B
x : B
hx : ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1
⊢ ∃ n ∈ S, x ^ ↑n = 1

Proof state:
case refine_2.intro.intro.inl.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ s ∈ S, m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
z : ℕ+
hy : m * z ∈ S
⊢ x ^ ↑(m * z) = 1

Tactic:
simp only [PNat.mul_coe, pow_mul, hxpow, one_pow]

Result:
no goals

Proof state:
case refine_2.intro.intro.inl.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ s ∈ S, m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
y : ℕ+
hy : y ∈ S
⊢ x ^ ↑y = 1

Tactic:
obtain ⟨z, rfl⟩ := h y hy

Result:
case refine_2.intro.intro.inl.intro.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ s ∈ S, m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
z : ℕ+
hy : m * z ∈ S
⊢ x ^ ↑(m * z) = 1

Proof state:
case refine_2.intro.intro.inl.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ s ∈ S, m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
y : ℕ+
hy : y ∈ S
⊢ ∃ n ∈ S, x ^ ↑n = 1

Tactic:
refine ⟨y, ⟨hy, ?_⟩⟩

Result:
case refine_2.intro.intro.inl.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
h : ∀ s ∈ S, m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
y : ℕ+
hy : y ∈ S
⊢ x ^ ↑y = 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 ∪ {n}) A B
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1} = ⊤

Tactic:
rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ 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 ∪ {n}) A B
⊢ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1} ≤ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1}

Proof state:
case refine_2.intro.intro.inr
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 ∪ {n}) A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
hm : m ∈ S
⊢ ∃ n ∈ S, x ^ ↑n = 1

Tactic:
exact ⟨m, ⟨hm, hxpow⟩⟩

Result:
no goals

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
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
refine
  ⟨fun H => of_union_of_dvd A B h hS, fun H => (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 ∪ {n}) A B
s : ℕ+
hs : s ∈ S
⊢ ∃ 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 ∪ {n}) A B
⊢ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 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 ∪ {n}) A B
⊢ adjoin A {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1} ≤ adjoin A {b | ∃ n ∈ S, b ^ ↑n = 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 ∪ {n}) A B
x : B
hx : x ∈ {b | ∃ n_1 ∈ S ∪ {n}, b ^ ↑n_1 = 1}
⊢ x ∈ {b | ∃ n ∈ S, b ^ ↑n = 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 ∪ {n}) A B
x : B
hx : ∃ n_1, (n_1 = n ∨ n_1 ∈ S) ∧ x ^ ↑n_1 = 1
⊢ ∃ n ∈ S, x ^ ↑n = 1

Tactic:
obtain ⟨m, rfl | hm, hxpow⟩ := hx

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

case refine_2.intro.intro.inr
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 ∪ {n}) A B
x : B
m : ℕ+
hxpow : x ^ ↑m = 1
hm : m ∈ S
⊢ ∃ n ∈ S, x ^ ↑n = 1