awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y_1 x y : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
ihx :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
ihy :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)
right :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (HMul.hMul (α := AlgebraicClosure K) (β := AlgebraicClosure K)
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K))
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x * y) : AlgebraicClosure K)

Tactic:
rw [map_mul]

Premises used: map_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y_1 x y : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
ihx :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
ihy :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)
⊢ Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (HMul.hMul (α := AlgebraicClosure K) (β := AlgebraicClosure K)
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K))

Tactic:
mul_mem ihx ihy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y_1 x y : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
ihx :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
ihy :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)
⊢ Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (HMul.hMul (α := AlgebraicClosure K) (β := AlgebraicClosure K)
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K))

Tactic:
exact mul_mem ihx ihy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y x : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
ihx :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
right :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x)⁻¹ : AlgebraicClosure K)
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x⁻¹ : AlgebraicClosure K)

Tactic:
rw [map_inv₀]

Premises used: map_inv₀
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y x : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
ihx :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x)⁻¹ : AlgebraicClosure K)

Tactic:
inv_mem ihx

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y x : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
ihx :
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x)⁻¹ : AlgebraicClosure K)

Tactic:
exact inv_mem ihx

Premises used: InvMemClass.inv_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : M), IsPrimitiveRoot r n
⊢ Nonempty (AlgEquiv.{w, z, u_1} K L ↥(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
have := IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K M h
  ⟨algEquiv S K L _⟩

Premises used: IsCyclotomicExtension.algEquiv, setOf, Membership.mem, Exists, Subtype, Ne, Nonempty.intro, And, HPow.hPow, IntermediateField.adjoin, IntermediateField.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot, OfNat.ofNat, Eq
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
rw :
  Eq (α := Subalgebra K L) (adjoin K ((HPow.hPow (α := K[X]) X n - 1).rootSet L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ Eq (α := Subalgebra K L) (adjoin K ((HPow.hPow (α := K[X]) X n - 1).rootSet L)) ⊤

Tactic:
rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]

Premises used: inferInstance, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Singleton.singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
e_s :
  (HPow.hPow (α := K[X]) X n - 1).rootSet L =
    {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ Eq (α := Subalgebra K L) (adjoin K ((HPow.hPow (α := K[X]) X n - 1).rootSet L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
congr
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
⊢ (HPow.hPow (α := K[X]) X n - 1).rootSet L =
    {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
Set.ext fun x => ?_

Premises used: Set.ext
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
e_s :
  ∀ (x : L),
    x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔
      Membership.mem (γ := Set L) {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1} x
⊢ (HPow.hPow (α := K[X]) X n - 1).rootSet L =
    {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
refine Set.ext fun x => ?_

Premises used: Set.ext
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
x : L
e_s : x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔ x ^ n = 1
⊢ x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔
    Membership.mem (γ := Set L) {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1} x

Tactic:
simp only [mem_singleton_iff, ne_eq, exists_eq_left, NeZero.ne, not_false_eq_true, true_and,
        mem_setOf_eq]

Premises used: exists_eq_left, Set.mem_setOf_eq, ne_eq, Set.mem_singleton_iff, not_false_eq_true, true_and, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
x : L
e_s : x ^ n = 1 → HPow.hPow (α := L[X]) X n - 1 ≠ 0
⊢ x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔ x ^ n = 1

Tactic:
simp only [mem_rootSet', map_sub, map_pow, aeval_one, aeval_X, sub_eq_zero, map_X,
        and_iff_right_iff_imp, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one]

Premises used: Polynomial.map_one, map_sub, sub_eq_zero, Polynomial.aeval_one, Polynomial.map_pow, Polynomial.map_X, map_pow, and_iff_right_iff_imp, Polynomial.mem_rootSet', Polynomial.map_sub, Polynomial.aeval_X
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
x : L
⊢ x ^ n = 1 → HPow.hPow (α := L[X]) X n - 1 ≠ 0

Tactic:
fun _ => X_pow_sub_C_ne_zero (NeZero.pos n) (1 : L)

Premises used: NeZero.pos, OfNat.ofNat, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
x : L
⊢ x ^ n = 1 → HPow.hPow (α := L[X]) X n - 1 ≠ 0

Tactic:
exact fun _ => X_pow_sub_C_ne_zero (NeZero.pos n) (1 : L)

Premises used: NeZero.pos, OfNat.ofNat, Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
rw :
  Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L)) ⊤

Tactic:
rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]

Premises used: inferInstance, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Singleton.singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
obtain :
  ∀ (ζ : L) (hζ : IsPrimitiveRoot ζ n),
    Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
      (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
obtain ⟨ζ : L, hζ⟩ :=
        IsCyclotomicExtension.exists_isPrimitiveRoot K L (mem_singleton n) (NeZero.ne _)

Premises used: Set.mem_singleton, IsCyclotomicExtension.exists_isPrimitiveRoot, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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
⊢ Eq (α := Algebra ℤ (CyclotomicField n ℚ)) (Ring.toIntAlgebra (CyclotomicField n ℚ)) (instAlgebra n ℤ ℚ)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, QuotientAddGroup.Quotient.addGroup._aux_9, RingCon.toQuotient, Polynomial.SplittingField, Finsupp.onFinset, Quotient, AddMonoidAlgebra.addAddCommGroup._aux_6, CyclotomicField, Quot.map, Quotient.map', Finsupp.mapRange, AddCon.Quotient, rfl, Finsupp.single
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : CharZero K
⊢ CharZero.{w} (CyclotomicField n K)

Tactic:
charZero_of_injective_algebraMap (algebraMap K _).injective

Premises used: Algebra.algebraMap, RingHom.injective, charZero_of_injective_algebraMap
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
⊢ NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)

Tactic:
have : NeZero (n : CyclotomicField n K) :=
    NeZero.nat_of_injective (algebraMap K _).injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
⊢ degree (cyclotomic n K) ≠ 0

Tactic:
have := (degree_cyclotomic_pos n K (NeZero.pos n)).ne'
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this rwa rwa₁ rwa₂ rwa₃ : degree (cyclotomic n K) ≠ 0
⊢ degree (R := SplittingField (cyclotomic n K))
      (map (algebraMap K (SplittingField (cyclotomic n K))) (cyclotomic n K)) ≠
    0

Tactic:
rwa [degree_map]

Premises used: Polynomial.degree_map
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
obtain :
  ∀ (ζ : SplittingField (cyclotomic n K))
    (hζ : eval ζ (map (algebraMap K (SplittingField (cyclotomic n K))) (cyclotomic n K)) = 0),
    IsCyclotomicExtension {n} K (CyclotomicField n K)
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
obtain ⟨ζ, hζ⟩ :=
    Splits.exists_eval_eq_zero (SplittingField.splits (cyclotomic n K)) (by rwa [degree_map])

Premises used: Polynomial.cyclotomic, Polynomial.SplittingField.splits, Polynomial.Splits.exists_eval_eq_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : eval ζ (map (algebraMap K (SplittingField (cyclotomic n K))) (cyclotomic n K)) = 0
⊢ IsPrimitiveRoot ζ n

Tactic:
rw [eval_map, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ

Premises used: Polynomial.eval_map, Polynomial.IsRoot.def, Polynomial.map_cyclotomic, Polynomial.isRoot_cyclotomic_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
⟨?_, ?_⟩

Premises used: IsCyclotomicExtension.mk
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
refine_1 :
  ∀ {n_1 : ℕ} (ha : Membership.mem (γ := Set ℕ) {n} n_1) (ha' : n_1 ≠ 0),
    ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n_1
refine_2 :
  ∀ (x : CyclotomicField n K),
    Membership.mem (γ := Subalgebra K (CyclotomicField n K))
      (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}) x
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
refine_1 : ∀ (ha' : n ≠ 0), ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n
⊢ ∀ {n_1 : ℕ} (ha : Membership.mem (γ := Set ℕ) {n} n_1) (ha' : n_1 ≠ 0),
    ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n_1

Tactic:
simp only [mem_singleton_iff, forall_eq]

Premises used: forall_eq, Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ ∀ (ha' : n ≠ 0), ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n

Tactic:
fun _ ↦ ⟨ζ, hζ⟩

Premises used: Exists.intro