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
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
h₁ h₂ h₃ 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 ^ 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})
    (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})

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
pos : ∀ (hn : n = 0), IsCyclotomicExtension (S ∪ {n}) A B
neg : ∀ (hn : ¬n = 0), IsCyclotomicExtension (S ∪ {n}) A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
pos : IsCyclotomicExtension (S ∪ {0}) A B
pos₁ : IsCyclotomicExtension ((S ∪ {0}) \ {0}) A B
pos₂ : IsCyclotomicExtension (S \ {0}) A B
pos₃ pos₄ pos₅ pos₆ : IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
rwa [hn, eq_self_sdiff_zero, Set.union_diff_right, ← eq_self_sdiff_zero]

Premises used: Set.union_diff_right, IsCyclotomicExtension.eq_self_sdiff_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
neg :
  (∀ n_1 ∈ S ∪ {n}, n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1) ∧
    Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
rw [iff_adjoin_eq_top]

Premises used: IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
neg : ∀ (m : ℕ) (hm₁ : m ∈ S ∪ {n}) (hm₂ : m ≠ 0), ∃ (r : B), IsPrimitiveRoot r m
neg₁ : LE.le.{v} (α := Subalgebra A B) ⊤ (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ (∀ n_1 ∈ S ∪ {n}, n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1) ∧
    Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤

Tactic:
refine ⟨fun m hm₁ hm₂ ↦ ?_, le_antisymm (by simp) ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₁ : m ∈ S ∪ {n}
hm₂ : m ≠ 0
neg : ∀ (hm₁ : m ∈ S), ∃ (r : B), IsPrimitiveRoot r m
neg₁ : ∀ [NeZero m] (hr : IsPrimitiveRoot r m) (hn : ¬m = 0), ∃ (r : B), IsPrimitiveRoot r m
⊢ ∃ (r : B), IsPrimitiveRoot r m

Tactic:
obtain hm₁ | rfl := hm₁

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₂ : m ≠ 0
hm₁ : m ∈ S
⊢ ∃ (r : B), IsPrimitiveRoot r m

Tactic:
exists_isPrimitiveRoot A B hm₁ hm₂

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₂ : m ≠ 0
hm₁ : m ∈ S
⊢ ∃ (r : B), IsPrimitiveRoot r m

Tactic:
exact exists_isPrimitiveRoot A B hm₁ hm₂

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- 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
hB : IsCyclotomicExtension S A B
r : B
m : ℕ
hm₂ : m ≠ 0
inst_3 : NeZero m
hr : IsPrimitiveRoot r m
hn : ¬m = 0
w : B
h : IsPrimitiveRoot r m
⊢ ∃ (r : B), IsPrimitiveRoot r m

Tactic:
use r
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
neg :
  LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ LE.le.{v} (α := Subalgebra A B) ⊤ (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
rw [← ((iff_adjoin_eq_top _ _ _).mp hB).2]

Premises used: And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ Subset.{v} (α := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
aesop
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
exact Algebra.adjoin_mono (by aesop)

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
(iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩

Premises used: Iff.mpr, And.intro, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
refine_1 : ∀ (s : ℕ) (hs : s ∈ S ∪ {n}) (hs' : s ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
refine_2 : Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤
⊢ IsCyclotomicExtension (S ∪ {n}) A B

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

Premises used: Iff.mpr, And.intro, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∪ {n}
hs' : s ≠ 0
⊢ s ∈ S ∨ s = n

Tactic:
rw [mem_union, mem_singleton_iff] at hs

Premises used: Set.mem_union, Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∪ {n}
hs' : s ≠ 0
hs₁ : s ∈ S ∨ s = n
⊢ s ≠ 0

Tactic:
rw [mem_union, mem_singleton_iff] at hs

Premises used: Set.mem_union, Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∨ s = n
hs' : s ≠ 0
refine_1 : ∀ (hs : s ∈ S), ∃ (r : B), IsPrimitiveRoot r s
refine_1₁ : ∀ [NeZero s] (h : ∃ s_1 ∈ S, s_1 ≠ 0 ∧ s ∣ s_1), ∃ (r : B), IsPrimitiveRoot r s
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
obtain hs | rfl := hs

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
hs : s ∈ S
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
H.exists_isPrimitiveRoot hs hs'

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
hs : s ∈ S
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
exact H.exists_isPrimitiveRoot hs hs'

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
h : ∃ s_1 ∈ S, s_1 ≠ 0 ∧ s ∣ s_1
refine_1 : ∀ (x : ℕ) (hm : s * x ∈ S) (hm' : s * x ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
⊢ ∃ (r : B), IsPrimitiveRoot r s

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

Premises used: rfl
-- 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
refine_1 : ∀ (ζ : B) (hζ : IsPrimitiveRoot ζ (s * x)), ∃ (r : B), IsPrimitiveRoot r s
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
obtain ⟨ζ, hζ⟩ := H.exists_isPrimitiveRoot hm hm'

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
⟨ζ ^ x, ?_⟩

Premises used: HPow.hPow, Exists.intro
-- 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
refine_1 : IsPrimitiveRoot (ζ ^ x) s
⊢ ∃ (r : B), IsPrimitiveRoot r s

Tactic:
refine ⟨ζ ^ 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
⊢ x ≠ 0

Tactic:
have h_xnz : x ≠ 0 := Nat.ne_zero_of_mul_ne_zero_right hm'
-- 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
h_xnz : x ≠ 0
⊢ IsPrimitiveRoot (ζ ^ x) (s * x / x)

Tactic:
have := hζ.pow_of_dvd h_xnz (dvd_mul_left x s)
-- 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
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
h_xnz : x ≠ 0
this : IsPrimitiveRoot (ζ ^ x) (s * x / x)
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (this : IsPrimitiveRoot (ζ ^ x) s), IsPrimitiveRoot (ζ ^ x) s
⊢ IsPrimitiveRoot (ζ ^ x) s

Tactic:
rwa [mul_div_cancel_right₀ _ h_xnz] at this

Premises used: mul_div_cancel_right₀
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
⊢ Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤

Tactic:
_root_.eq_top_iff.2 ?_

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
refine_2 : LE.le.{v} (α := Subalgebra A B) ⊤ (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤

Tactic:
refine _root_.eq_top_iff.2 ?_

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
refine_2 :
  LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ LE.le.{v} (α := Subalgebra A B) ⊤ (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})

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

Premises used: And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
⊢ LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
adjoin_mono fun x hx ↦ ?_

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
refine_2 :
  ∀ (x : B) (hx : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x),
    Membership.mem (γ := Set B) {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} x
⊢ LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
refine adjoin_mono fun x hx ↦ ?_

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
x : B
hx : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x
refine_2 : ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1
⊢ Membership.mem (γ := Set B) {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} x

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

Premises used: Set.mem_setOf_eq, Set.mem_insert_iff, Set.union_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
x : B
hx : ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1
refine_2 : ∀ (m : ℕ) (hm : m ∈ S) (hm' : m ≠ 0 ∧ x ^ m = 1), ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1
⊢ ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1

Tactic:
obtain ⟨m, hm, hm'⟩ := hx
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
x : B
m : ℕ
hm : m ∈ S
hm' : m ≠ 0 ∧ x ^ m = 1
⊢ ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1

Tactic:
⟨m, ⟨Or.inr hm, hm'⟩⟩

Premises used: And.intro, Exists.intro, Or.inr
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
x : B
m : ℕ
hm : m ∈ S
hm' : m ≠ 0 ∧ x ^ m = 1
⊢ ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1

Tactic:
exact ⟨m, ⟨Or.inr hm, hm'⟩⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2
      ⟨fun s hs ↦ ?_, ?_⟩⟩

Premises used: Iff.mpr, IsCyclotomicExtension.of_union_of_dvd, And.intro, Iff.intro, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
refine_1 : ∀ (H : IsCyclotomicExtension (S ∪ {n}) A B) (s : ℕ) (hs : s ∈ S), s ≠ 0 → ∃ (r : B), IsPrimitiveRoot r s
refine_2 :
  ∀ (H : IsCyclotomicExtension (S ∪ {n}) A B),
    Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
refine
    ⟨fun H ↦ of_union_of_dvd A B h, fun H => (iff_adjoin_eq_top _ A _).2
      ⟨fun s hs ↦ ?_, ?_⟩⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
s : ℕ
hs : s ∈ S
⊢ s ≠ 0 → ∃ (r : B), IsPrimitiveRoot r s

Tactic:
H.exists_isPrimitiveRoot (subset_union_left hs)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, Set.subset_union_left
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
s : ℕ
hs : s ∈ S
⊢ s ≠ 0 → ∃ (r : B), IsPrimitiveRoot r s

Tactic:
exact H.exists_isPrimitiveRoot (subset_union_left hs)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, Set.subset_union_left
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
refine_2 :
  LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤

Tactic:
rw [_root_.eq_top_iff, ← ((iff_adjoin_eq_top _ A B).1 H).2]

Premises used: eq_top_iff, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
⊢ LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
adjoin_mono fun x hx => ?_

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
refine_2 :
  ∀ (x : B) (hx : Membership.mem (γ := Set B) {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} x),
    Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x
⊢ LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
refine adjoin_mono fun x hx => ?_

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
hx : Membership.mem (γ := Set B) {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1} x
⊢ ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1

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

Premises used: Set.mem_setOf_eq, Set.mem_insert_iff, Set.union_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
hx : ∃ (n_1 : ℕ), (n_1 = n ∨ n_1 ∈ S) ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1
refine_2 :
  ∀ (m : ℕ) (hxpow : m ≠ 0 ∧ x ^ m = 1) [NeZero m] (h : ∃ s ∈ S, s ≠ 0 ∧ m ∣ s)
    (H : IsCyclotomicExtension (S ∪ {m}) A B), ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1
refine_2₁ : ∀ (m : ℕ) (hxpow : m ≠ 0 ∧ x ^ m = 1) (hm : m ∈ S), ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

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

Premises used: rfl
-- 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
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
inst_3 : NeZero m
h : ∃ s ∈ S, s ≠ 0 ∧ m ∣ s
H : IsCyclotomicExtension (S ∪ {m}) A B
refine_2 : ∀ (z : ℕ) (hy : m * z ∈ S) (hy' : m * z ≠ 0), ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

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

Premises used: rfl
-- 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
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
inst_3 : NeZero m
H : IsCyclotomicExtension (S ∪ {m}) A B
z : ℕ
hy : m * z ∈ S
hy' : m * z ≠ 0
⊢ x ^ (m * z) = 1

Tactic:
simp only [pow_mul, hxpow, one_pow]

Premises used: one_pow, pow_mul
-- 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
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
inst_3 : NeZero m
H : IsCyclotomicExtension (S ∪ {m}) A B
z : ℕ
hy : m * z ∈ S
hy' : m * z ≠ 0
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

Tactic:
exact ⟨_, ⟨hy, hy', by simp only [pow_mul, hxpow, one_pow]⟩⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
hm : m ∈ S
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

Tactic:
⟨m, ⟨hm, hxpow⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension (S ∪ {n}) A B
x : B
m : ℕ
hxpow : m ≠ 0 ∧ x ^ m = 1
hm : m ∈ S
⊢ ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1

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