-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem iff_union_singleton_one :
    IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Proof state:
case inr.refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension ∅ A B
⊢ adjoin A {b | ∃ n ∈ {1}, b ^ ↑n = 1} = ⊤

Tactic:
simp [adjoin_singleton_one, empty]

Result:
no goals

Proof state:
case inr.refine_2
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension {1} A B
⊢ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1} = ⊤

Tactic:
simp [@singleton_one A B _ _ _ H]

Result:
no goals

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
obtain hS | rfl := S.eq_empty_or_nonempty.symm

Result:
case inl
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : S.Nonempty
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

case inr
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension (∅ ∪ {1}) A B

Proof state:
case inr.refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension ∅ A B
⊢ IsCyclotomicExtension {1} A B

Tactic:
refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs => ⟨1, by simp [mem_singleton_iff.1 hs]⟩, ?_⟩

Result:
case inr.refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension ∅ A B
⊢ adjoin A {b | ∃ n ∈ {1}, b ^ ↑n = 1} = ⊤

Proof state:
case inr
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B

Tactic:
refine ⟨fun H => ?_, fun H => ?_⟩

Result:
case inr.refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension ∅ A B
⊢ IsCyclotomicExtension {1} A B

case inr.refine_2
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension ∅ A B

Proof state:
case inr.refine_2
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension ∅ A B

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

Result:
case inr.refine_2
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension {1} A B
⊢ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1} = ⊤

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
H : IsCyclotomicExtension ∅ A B
s : ℕ+
hs : s ∈ {1}
⊢ IsPrimitiveRoot 1 ↑s

Tactic:
simp [mem_singleton_iff.1 hs]

Result:
no goals

Proof state:
case inl
S : Set ℕ+
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
hS : S.Nonempty
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
exact iff_union_of_dvd _ _ (fun s _ => one_dvd _) hS

Result:
no goals

Proof state:
case inr
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension (∅ ∪ {1}) A B

Tactic:
rw [empty_union]

Result:
case inr
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B