awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb :
  Membership.mem.{w, w} (α := C) (γ := Subalgebra A C)
    (adjoin A (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    ((algebraMap B C : (a : B) → C) b : C)
y : C
b₁ : B
h₁ : (f : (a : B) → C) b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
rw : HPow.hPow (α := C) ((f : (a : B) → C) b₁ : C) n = 1
rw₁ : Eq.{w + 1} (α := C) ((f : (a : B) → C) (b₁ ^ n) : C) (1 : C)
rw₂ : Eq.{w + 1} (α := C) ((f : (a : B) → C) 1 : C) (1 : C)
rw₃ rw₄ : Eq.{w + 1} (α := C) 1 1
⊢ y ^ n = 1

Tactic:
rw [← h₁, ← map_pow, hn.2.2, map_one]

Premises used: map_pow, And.right, map_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb :
  Membership.mem.{w, w} (α := C) (γ := Subalgebra A C)
    (adjoin A (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    ((algebraMap B C : (a : B) → C) b : C)
y : C
b₁ : B
h₁ : (f : (a : B) → C) b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
⊢ Membership.mem (γ := Set C) {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} y

Tactic:
exact ⟨n, ⟨mem_union_left T hn.1, hn.2.1, by rw [← h₁, ← map_pow, hn.2.2, map_one]⟩⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
⊢ Subsingleton.{v + 1} (Subalgebra A B)

Tactic:
have : Subsingleton (Subalgebra A B) := inferInstance
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
⊢ IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}

Tactic:
⟨fun ⟨hprim, _⟩ ↦ ?_, fun hS ↦ ?_⟩

Premises used: Insert.insert, HasSubset.Subset, Iff.intro, _private.0.IsCyclotomicExtension.subsingleton_iff.match_1, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
refine_1 :
  IsCyclotomicExtension S A B →
    ∀ (hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n),
      (∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) → S ⊆ {0, 1}
refine_2 : ∀ (hS : S ⊆ {0, 1}), IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}

Tactic:
refine ⟨fun ⟨hprim, _⟩ ↦ ?_, fun hS ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
⊢ S ⊆ {0, 1}

Tactic:
subset_pair_iff.mpr fun s hs ↦ or_iff_not_imp_left.mpr fun hs' ↦ ?_

Premises used: Iff.mpr, Set.subset_pair_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
refine_1 : ∀ (s : ℕ) (hs : s ∈ S) (hs' : ¬s = 0), s = 1
⊢ S ⊆ {0, 1}

Tactic:
refine subset_pair_iff.mpr fun s hs ↦ or_iff_not_imp_left.mpr fun hs' ↦ ?_

Premises used: Iff.mpr, Set.subset_pair_iff, Classical.or_iff_not_imp_left
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
s : ℕ
hs : s ∈ S
hs' : ¬s = 0
refine_1 : ∀ (ζ : B) (hζ : IsPrimitiveRoot ζ s), s = 1
⊢ s = 1

Tactic:
obtain ⟨ζ, hζ⟩ := hprim hs hs'
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
s : ℕ
hs : s ∈ S
hs' : ¬s = 0
ζ : B
hζ : IsPrimitiveRoot ζ s
⊢ s = 1

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

Premises used: cast, Eq.refl, IsPrimitiveRoot.unique, IsPrimitiveRoot.of_subsingleton, OfNat.ofNat, Eq
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
s : ℕ
hs : s ∈ S
hs' : ¬s = 0
ζ : B
hζ : IsPrimitiveRoot ζ s
⊢ s = 1

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

Premises used: IsPrimitiveRoot.unique, IsPrimitiveRoot.of_subsingleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
x : B
⊢ Membership.mem (γ := Subalgebra A B) ⊤ x

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

Premises used: Algebra.mem_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
x : B
⊢ Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x

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

Premises used: Algebra.mem_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
refine_2 : ∀ {s : ℕ} (hs : s ∈ S) (hs' : s ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
⊢ IsCyclotomicExtension S A B

Tactic:
refine ⟨fun {s} hs hs' ↦ ?_, fun x ↦ by convert! (mem_top (R := A) : x ∈ ⊤)⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
s : ℕ
hs : s ∈ S
hs' : s ≠ 0
⊢ s = 1

Tactic:
have : s = 1 := (subset_pair_iff.mp hS s hs).resolve_left hs'
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this_1 : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
s : ℕ
hs : s ∈ S
hs' : s ≠ 0
this : s = 1
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
⟨0, this ▸ IsPrimitiveRoot.of_subsingleton 0⟩

Premises used: Eq.rec, Exists.intro, IsPrimitiveRoot.of_subsingleton, OfNat.ofNat, Eq.symm
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this_1 : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
s : ℕ
hs : s ∈ S
hs' : s ≠ 0
this : s = 1
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
exact ⟨0, this ▸ IsPrimitiveRoot.of_subsingleton 0⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
refine_1 :
  LE.le.{v} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
refine_2 :
  LE.le.{v} (α := Set B) ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
    {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
⊢ Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
refine_1 : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x
⊢ Membership.mem (γ := Set B) ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) x

Tactic:
left
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x

Tactic:
⟨n, hn₁, hnpow⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x

Tactic:
exact ⟨n, hn₁, hnpow⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
refine_1 : Membership.mem (γ := Set B) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1} x
⊢ Membership.mem (γ := Set B) ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) x

Tactic:
right
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1} x

Tactic:
⟨n, hn₂, hnpow⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1} x

Tactic:
exact ⟨n, hn₂, hnpow⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ x ^ n = 1
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} x

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

Premises used: Set.Mem, setOf, And.right, And.left, And.intro, Exists.intro, Or.inl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ x ^ n = 1
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} x

Tactic:
exact ⟨n, Or.inl hn.1, hn.2⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ T ∧ n ≠ 0 ∧ x ^ n = 1
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} x

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

Premises used: Set.Mem, setOf, And.right, And.left, And.intro, Exists.intro, Or.inr
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hn : n ∈ T ∧ n ≠ 0 ∧ x ^ n = 1
⊢ Membership.mem (γ := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} x

Tactic:
exact ⟨n, Or.inr hn.1, hn.2⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})

Tactic:
have : {b : B | ∃ n : ℕ, n ∈ S ∪ T ∧ n ≠ 0 ∧ b ^ n = 1} =
      {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1} ∪
        {b : B | ∃ n : ℕ, n ∈ T ∧ n ≠ 0 ∧ b ^ n = 1} := by
    refine le_antisymm ?_ ?_
    · rintro x ⟨n, hn₁ | hn₂, hnpow⟩
      · left; exact ⟨n, hn₁, hnpow⟩
      · right; exact ⟨n, hn₂, hnpow⟩
    · rintro x (⟨n, hn⟩ | ⟨n, hn⟩)
      · exact ⟨n, Or.inl hn.1, hn.2⟩
      · exact ⟨n, Or.inr hn.1, hn.2⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
⊢ IsCyclotomicExtension T (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B

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

Premises used: IsCyclotomicExtension.mk, Set.mem_union_right, And.left, isCyclotomicExtension_iff, Iff.mp, Union.union
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
refine :
  ∀ (b : B),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
⊢ IsCyclotomicExtension T (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B

Tactic:
refine ⟨fun hn => ((isCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
b : B
⊢ Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) b

Tactic:
replace h := ((isCyclotomicExtension_iff _ _ _).1 h).2 b
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
b : B
h : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) b
rwa :
  ∀
    (h :
      Membership.mem (γ := Subalgebra A B)
        (adjoin A ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})) b),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
rwa₁ :
  ∀
    (h :
      Membership.mem (γ := Subalgebra A B)
        (Subalgebra.restrictScalars A (S := ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
          (adjoin ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}))
        b),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (h :
      Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B)
        (adjoin ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
⊢ Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b

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

Premises used: Subalgebra.mem_restrictScalars, Algebra.adjoin_union_eq_adjoin_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
⊢ IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

Tactic:
⟨fun {n} hn hn' => ?_, fun b => ?_⟩

Premises used: IsCyclotomicExtension.mk
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
refine_1 :
  ∀ {n : ℕ} (hn : n ∈ S) (hn' : n ≠ 0), ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
refine_2 :
  ∀ (b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})),
    Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
      (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) b
⊢ IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})

Tactic:
refine ⟨fun {n} hn hn' => ?_, fun b => ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
refine_1 :
  ∀ (b : B) (hb : IsPrimitiveRoot b n), ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n

Tactic:
obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) hn'

Premises used: And.left, isCyclotomicExtension_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
b : B
hb : IsPrimitiveRoot b n
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n

Tactic:
⟨⟨b, subset_adjoin ⟨n, hn, hn', hb.pow_eq_one⟩⟩, ?_⟩

Premises used: Algebra.subset_adjoin, Subtype.mk, And.intro, Exists.intro, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
b : B
hb : IsPrimitiveRoot b n
refine_1 :
  IsPrimitiveRoot (M := ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) x) b ⋯)
    n
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n

Tactic:
refine ⟨⟨b, subset_adjoin ⟨n, hn, hn', hb.pow_eq_one⟩⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
b : B
hb : IsPrimitiveRoot b n
refine_1 :
  IsPrimitiveRoot
    (↑(Subtype.mk (p := fun (x : B) ↦
          Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) x) b ⋯) :
      B)
    n
refine_1₁ refine_1₂ refine_1₃ refine_1₄ : IsPrimitiveRoot b n
⊢ IsPrimitiveRoot (M := ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) x) b ⋯)
    n

Tactic:
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]

Premises used: Subtype.coe_mk, IsPrimitiveRoot.coe_submonoidClass_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) ⊤ b

Tactic:
mem_top (R := A) (x := b)

Premises used: Algebra.mem_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
h₁ :
  Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) b

Tactic:
convert! mem_top (R := A) (x := b)

Premises used: Algebra.mem_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
h₁ :
  Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {a : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ a_1 ∈ S, a_1 ≠ 0 ∧ (↑a : B) ^ a_1 = 1})
⊢ Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤

Tactic:
rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq]

Premises used: Set.preimage_setOf_eq, Algebra.adjoin_adjoin_coe_preimage