awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
⊢ NeZero.{w} (R := K) (↑a : K)

Tactic:
have := h a ha ha'
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
obtain :
  ∀ (r : K) (hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)), ∃ (r : K), IsPrimitiveRoot r a
⊢ ∃ (r : K), IsPrimitiveRoot r a

Tactic:
obtain ⟨r, hr⟩ := IsSepClosed.exists_aeval_eq_zero K _
    (degree_cyclotomic_pos a K (Nat.pos_of_ne_zero ha')).ne' (separable_cyclotomic a K)

Premises used: LT.lt.ne', Nat.pos_of_ne_zero, Polynomial.separable_cyclotomic, Polynomial.degree_cyclotomic_pos, IsSepClosed.exists_aeval_eq_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
r : K
hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)
rwa : ∀ (hr : eval r (cyclotomic a K) = 0), IsPrimitiveRoot r a
rwa₁ : ∀ (hr : IsRoot (cyclotomic a K) r), IsPrimitiveRoot r a
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hr : IsPrimitiveRoot r a), IsPrimitiveRoot r a
⊢ IsPrimitiveRoot r a

Tactic:
rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr

Premises used: Polynomial.IsRoot.def, Polynomial.coe_aeval_eq_eval, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
r : K
hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)
⊢ ∃ (r : K), IsPrimitiveRoot r a

Tactic:
exact ⟨r, by rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S_1 T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : IsSepClosed K
inst_8 : CharZero K
S : Set ℕ
rw : IsCyclotomicExtension (S \ {0}) K K
⊢ IsCyclotomicExtension S K K

Tactic:
rw [IsCyclotomicExtension.eq_self_sdiff_zero]

Premises used: IsCyclotomicExtension.eq_self_sdiff_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S_1 T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : IsSepClosed K
inst_8 : CharZero K
S : Set ℕ
⊢ IsCyclotomicExtension (S \ {0}) K K

Tactic:
IsSepClosed.isCyclotomicExtension _ K fun _ _ h ↦ ⟨Nat.cast_ne_zero.mpr h⟩

Premises used: Iff.mpr, NeZero.mk, IsSepClosed.isCyclotomicExtension, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S_1 T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : IsSepClosed K
inst_8 : CharZero K
S : Set ℕ
⊢ IsCyclotomicExtension (S \ {0}) K K

Tactic:
exact IsSepClosed.isCyclotomicExtension _ K fun _ _ h ↦ ⟨Nat.cast_ne_zero.mpr h⟩

Premises used: Iff.mpr, NeZero.mk, IsSepClosed.isCyclotomicExtension, Nat.cast_ne_zero
-- 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 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
obtain : ∀ (η : ↥C) (hη : IsPrimitiveRoot η m), ζ ∈ C
⊢ ζ ∈ C

Tactic:
obtain ⟨η, hη⟩ := h.1 h₁ h₂

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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot η m
⊢ IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m

Tactic:
replace hη := hη.map_of_injective (FaithfulSMul.algebraMap_injective C B)
-- 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 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
⊢ NeZero m

Tactic:
have : NeZero m := ⟨h₂⟩
-- 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 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
this : NeZero m
obtain :
  ∀ k < m,
    ∀ (hζ : HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ^ m = 1),
      HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ∈ C
⊢ ζ ∈ C

Tactic:
obtain ⟨k, _, rfl⟩ := hη.eq_pow_of_pow_eq_one hζ

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one, 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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
h₁ : m ∈ S
h₂ : m ≠ 0
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
this : NeZero m
k : ℕ
left : k < m
hζ : HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ^ m = 1
rw : Membership.mem (α := B) C ((algebraMap (↥C) B : (a : ↥C) → B) (η ^ k) : B)
⊢ HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ∈ C

Tactic:
rw [← map_pow]

Premises used: map_pow
-- 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 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
h₁ : m ∈ S
h₂ : m ≠ 0
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
this : NeZero m
k : ℕ
left : k < m
hζ : HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ^ m = 1
⊢ Membership.mem (α := B) C ((algebraMap (↥C) B : (a : ↥C) → B) (η ^ k) : B)

Tactic:
Subalgebra.pow_mem _ η.prop _

Premises used: Set.Mem, Subalgebra.pow_mem, Subtype.prop
-- 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 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
h₁ : m ∈ S
h₂ : m ≠ 0
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
this : NeZero m
k : ℕ
left : k < m
hζ : HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ^ m = 1
⊢ Membership.mem (α := B) C ((algebraMap (↥C) B : (a : ↥C) → B) (η ^ k) : B)

Tactic:
exact Subalgebra.pow_mem _ η.prop _

Premises used: Subalgebra.pow_mem, Subtype.prop
-- 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
⊢ IsCyclotomicExtension.{u, v} S A ↥C ↔ C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
⟨fun h ↦ ?_, fun h ↦ h ▸ isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S A B hS⟩

Premises used: Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, Eq.rec, Iff.intro, 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
refine : ∀ (h : IsCyclotomicExtension.{u, v} S A ↥C), C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ IsCyclotomicExtension.{u, v} S A ↥C ↔ C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S A B 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
⊢ Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤

Tactic:
have := congr_arg (Subalgebra.map C.val) ((IsCyclotomicExtension.iff_adjoin_eq_top _ _ _).mp h).2
-- 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
rw :
  Eq (α := Subalgebra A B) (adjoin A (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
⊢ C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
rw [← Subalgebra.range_val C, ← Algebra.map_top, ← this, AlgHom.map_adjoin]

Premises used: Subalgebra.range_val, AlgHom.map_adjoin, Algebra.map_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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
e_s :
  Eq (α := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ Eq (α := Subalgebra A B) (adjoin A (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})

Tactic:
congr
-- 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
e_s :
  ∀ (x : B),
    Membership.mem (γ := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x ↔
      Membership.mem (γ := Set B) {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x
⊢ Eq (α := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
ext
-- 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x : B
e_s : ∀ x_1 ∈ S, ¬x_1 = 0 → x ^ x_1 = 1 → x ∈ C
⊢ Membership.mem (γ := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x ↔
    Membership.mem (γ := Set B) {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x

Tactic:
simp only [Subalgebra.coe_val, ne_eq, ← Subalgebra.coe_eq_one, SubmonoidClass.coe_pow,
    Set.mem_image, Set.mem_setOf_eq, Subtype.exists, exists_and_left, exists_prop,
    exists_eq_right_right, and_iff_left_iff_imp, forall_exists_index, and_imp]

Premises used: exists_eq_right_right, and_imp, Set.mem_image, Subtype.exists, forall_exists_index, exists_and_left, Set.mem_setOf_eq, exists_prop, ne_eq, Subalgebra.coe_eq_one, Subalgebra.coe_val, SubmonoidClass.coe_pow, and_iff_left_iff_imp
-- 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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x : B
⊢ ∀ x_1 ∈ S, ¬x_1 = 0 → x ^ x_1 = 1 → x ∈ C

Tactic:
fun n hn₁ hn₂ hx ↦ h.mem_of_pow_eq_one S C hn₁ hn₂ hx

Premises used: IsCyclotomicExtension.mem_of_pow_eq_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 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x : B
⊢ ∀ x_1 ∈ S, ¬x_1 = 0 → x ^ x_1 = 1 → x ∈ C

Tactic:
exact fun n hn₁ hn₂ hx ↦ h.mem_of_pow_eq_one S C hn₁ hn₂ hx

Premises used: IsCyclotomicExtension.mem_of_pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
rw : C = adjoin A {x : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]
hS : ∀ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 → n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1
⊢ IsCyclotomicExtension.{u, v} {n} A ↥C ↔ C = A[ζ]

Tactic:
rw [isCyclotomicExtension_iff_eq_adjoin]

Premises used: isCyclotomicExtension_iff_eq_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
simp : C = adjoin A {x : B | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]
⊢ C = adjoin A {x : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]

Tactic:
simp only [Set.mem_singleton_iff, exists_eq_left]

Premises used: exists_eq_left, Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
this : Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
rw rw₁ : C = A[ζ] ↔ C = A[ζ]
⊢ C = adjoin A {x : B | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
suffices : Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
⊢ C = adjoin A {x : B | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]

Tactic:
suffices adjoin A {b | n ≠ 0 ∧ b ^ n = 1} = adjoin A {ζ} by rw [this]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
a : LE.le (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
a₁ : LE.le (α := Subalgebra A B) A[ζ] (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})
⊢ Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ LE.le (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]

Tactic:
adjoin_le fun x ⟨_, hx⟩ ↦ ?_

Premises used: Algebra.adjoin, Membership.mem, SetLike.coe, Algebra.adjoin_le, _private.0.isCyclotomicExtension_singleton_iff_eq_adjoin.match_1, Singleton.singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
a :
  ∀ (x : B), Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x → n ≠ 0 → ∀ (hx : x ^ n = 1), x ∈ (↑A[ζ] : Set B)
⊢ LE.le (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]

Tactic:
refine adjoin_le fun x ⟨_, hx⟩ ↦ ?_
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
h : Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x
left : n ≠ 0
hx : x ^ n = 1
a :
  ∀ k < n,
    Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} (ζ ^ k) → ∀ (hx : (ζ ^ k) ^ n = 1), ζ ^ k ∈ (↑A[ζ] : Set B)
⊢ x ∈ (↑A[ζ] : Set B)

Tactic:
obtain ⟨k, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
left : n ≠ 0
k : ℕ
left_1 : k < n
h : Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} (ζ ^ k)
hx : (ζ ^ k) ^ n = 1
⊢ ζ ^ k ∈ (↑A[ζ] : Set B)

Tactic:
Subalgebra.pow_mem _ (self_mem_adjoin_singleton A ζ) _

Premises used: Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
left : n ≠ 0
k : ℕ
left_1 : k < n
h : Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} (ζ ^ k)
hx : (ζ ^ k) ^ n = 1
⊢ ζ ^ k ∈ (↑A[ζ] : Set B)

Tactic:
exact Subalgebra.pow_mem _ (self_mem_adjoin_singleton A ζ) _

Premises used: Subalgebra.pow_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ LE.le (α := Subalgebra A B) A[ζ] (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})

Tactic:
adjoin_mono <| Set.singleton_subset_iff.mpr ⟨NeZero.ne n, hζ.pow_eq_one⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Algebra.adjoin_mono, And.intro, IsPrimitiveRoot.pow_eq_one, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ LE.le (α := Subalgebra A B) A[ζ] (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})

Tactic:
exact adjoin_mono <| Set.singleton_subset_iff.mpr ⟨NeZero.ne n, hζ.pow_eq_one⟩

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ ∀ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 → n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1

Tactic:
simpa only [Set.mem_singleton_iff, ne_eq, forall_eq, NeZero.ne n, not_false_eq_true,
      forall_const] using ⟨ζ, hζ⟩

Premises used: forall_eq, ne_eq, Set.mem_singleton_iff, forall_const, not_false_eq_true, NeZero.ne
-- 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 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
n : ℕ
hn₁ : n ∈ S
hn₂ : n ≠ 0
obtain : ∀ (ζ : ↥C₁) (hζ : IsPrimitiveRoot ζ n), ∃ (x : B), IsPrimitiveRoot x n
⊢ ∃ (x : B), IsPrimitiveRoot x n

Tactic:
obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂

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
inst_3 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
n : ℕ
hn₁ : n ∈ S
hn₂ : n ≠ 0
ζ : ↥C₁
hζ : IsPrimitiveRoot ζ n
⊢ ∃ (x : B), IsPrimitiveRoot x n

Tactic:
⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr hζ⟩

Premises used: Iff.mpr, IsPrimitiveRoot.coe_submonoidClass_iff, Exists.intro, Subtype.val
-- 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 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
n : ℕ
hn₁ : n ∈ S
hn₂ : n ≠ 0
ζ : ↥C₁
hζ : IsPrimitiveRoot ζ n
⊢ ∃ (x : B), IsPrimitiveRoot x n

Tactic:
exact ⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr hζ⟩
-- 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 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
⊢ ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : n ≠ 0), ∃ (x : B), IsPrimitiveRoot x n

Tactic:
have hC (n) (hn₁ : n ∈ S) (hn₂ : n ≠ 0) : ∃ x : B, IsPrimitiveRoot x n := by
    obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂
    exact ⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr hζ⟩
-- 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 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
hC : ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : n ≠ 0), ∃ (x : B), IsPrimitiveRoot x n
rw : adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = C₂
rw₁ rw₂ :
  Eq.{v + 1} (α := Subalgebra A B) (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
⊢ C₁ = C₂

Tactic:
rw [(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁,
    (isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp h₂]

Premises used: isCyclotomicExtension_iff_eq_adjoin, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
out : n₁ ≠ 0
⊢ NeZero n₁

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h₁ : IsCyclotomicExtension.{u, v} {0} A ↥C₁
h : 0 ∣ n₂
⊢ False

Tactic:
NeZero.ne n₂ <| eq_zero_of_zero_dvd h

Premises used: eq_zero_of_zero_dvd, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h₁ : IsCyclotomicExtension.{u, v} {0} A ↥C₁
h : 0 ∣ n₂
⊢ False

Tactic:
exact NeZero.ne n₂ <| eq_zero_of_zero_dvd h

Premises used: eq_zero_of_zero_dvd, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
⊢ NeZero n₁

Tactic:
have : NeZero n₁ := by
    constructor
    rintro rfl
    exact NeZero.ne n₂ <| eq_zero_of_zero_dvd h