-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem subsingleton_iff [Subsingleton B] : IsCyclotomicExtension S A B ↔ S = { } ∨ S = {1}

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
⊢ IsCyclotomicExtension S A B ↔ S = ∅ ∨ S = {1}

Tactic:
have : Subsingleton (Subalgebra A B) := inferInstance

Result:
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension S A B ↔ S = ∅ ∨ S = {1}

Proof state:
case mp.mk.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑t
⊢ t ∈ {1}

Tactic:
rw [mem_singleton_iff, ← PNat.coe_eq_one_iff]

Result:
case mp.mk.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑t
⊢ ↑t = 1

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
x : B
⊢ x ∈ adjoin A {b | ∃ n ∈ ∅, b ^ ↑n = 1}

Tactic:
convert (mem_top (R := A) : x ∈ ⊤)

Result:
no goals

Proof state:
case mpr.inr
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension {1} A B

Tactic:
rw [iff_singleton]

Result:
case mpr.inr
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ (∃ r, IsPrimitiveRoot r ↑1) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ ↑1 = 1}

Proof state:
case mpr.inl
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension ∅ A B

Tactic:
exact ⟨fun h => h.elim, fun x => by convert (mem_top (R := A) : x ∈ ⊤)⟩

Result:
no goals

Proof state:
case mp.mk
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
⊢ S = ∅ ∨ S = {1}

Tactic:
rw [← subset_singleton_iff_eq]

Result:
case mp.mk
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
⊢ S ⊆ {1}

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension S A B ↔ S = ∅ ∨ S = {1}

Tactic:
constructor

Result:
case mp
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension S A B → S = ∅ ∨ S = {1}

case mpr
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ S = ∅ ∨ S = {1} → IsCyclotomicExtension S A B

Proof state:
case mpr
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ S = ∅ ∨ S = {1} → IsCyclotomicExtension S A B

Tactic:
rintro (rfl | rfl)

Result:
case mpr.inl
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension ∅ A B

case mpr.inr
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension {1} A B

Proof state:
case mp.mk
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
⊢ t ∈ {1}

Tactic:
obtain ⟨ζ, hζ⟩ := hprim ht

Result:
case mp.mk.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑t
⊢ t ∈ {1}

Proof state:
case mp.mk.intro
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
ζ : B
hζ : IsPrimitiveRoot ζ ↑t
⊢ ↑t = 1

Tactic:
exact mod_cast hζ.unique (IsPrimitiveRoot.of_subsingleton ζ)

Result:
no goals

Proof state:
case mp
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ IsCyclotomicExtension S A B → S = ∅ ∨ S = {1}

Tactic:
rintro ⟨hprim, -⟩

Result:
case mp.mk
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
⊢ S = ∅ ∨ S = {1}

Proof state:
case mp.mk
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
⊢ S ⊆ {1}

Tactic:
intro t ht

Result:
case mp.mk
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
hprim : ∀ {n : ℕ+}, n ∈ S → ∃ r, IsPrimitiveRoot r ↑n
t : ℕ+
ht : t ∈ S
⊢ t ∈ {1}

Proof state:
case mpr.inr
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
⊢ (∃ r, IsPrimitiveRoot r ↑1) ∧ ∀ (x : B), x ∈ adjoin A {b | b ^ ↑1 = 1}

Tactic:
exact ⟨⟨0, IsPrimitiveRoot.of_subsingleton 0⟩,
  fun x => by convert (mem_top (R := A) : x ∈ ⊤)⟩

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Subsingleton B
this : Subsingleton (Subalgebra A B)
x : B
⊢ x ∈ adjoin A {b | b ^ ↑1 = 1}

Tactic:
convert (mem_top (R := A) : x ∈ ⊤)

Result:
no goals