awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b₁ b₂ : B
h_1 : Membership.mem (γ := Subalgebra A B) A[ζ] b₁
h_2 : Membership.mem (γ := Subalgebra A B) A[ζ] b₂
hb₁ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₁ h_1)
hb₂ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₂ h_2)
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) (b₁ + b₂) ⋯)

Tactic:
Subalgebra.add_mem _ hb₁ hb₂

Premises used: Set.Mem, Subalgebra.add_mem, setOf
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b₁ b₂ : B
h_1 : Membership.mem (γ := Subalgebra A B) A[ζ] b₁
h_2 : Membership.mem (γ := Subalgebra A B) A[ζ] b₂
hb₁ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₁ h_1)
hb₂ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₂ h_2)
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) (b₁ + b₂) ⋯)

Tactic:
exact Subalgebra.add_mem _ hb₁ hb₂

Premises used: Subalgebra.add_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b₁ b₂ : B
h_1 : Membership.mem (γ := Subalgebra A B) A[ζ] b₁
h_2 : Membership.mem (γ := Subalgebra A B) A[ζ] b₂
hb₁ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₁ h_1)
hb₂ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₂ h_2)
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) (b₁ * b₂) ⋯)

Tactic:
Subalgebra.mul_mem _ hb₁ hb₂

Premises used: Subalgebra.mul_mem, Set.Mem, setOf
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b₁ b₂ : B
h_1 : Membership.mem (γ := Subalgebra A B) A[ζ] b₁
h_2 : Membership.mem (γ := Subalgebra A B) A[ζ] b₂
hb₁ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₁ h_1)
hb₂ :
  Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₂ h_2)
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) (b₁ * b₂) ⋯)

Tactic:
exact Subalgebra.mul_mem _ hb₁ hb₂

Premises used: Subalgebra.mul_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
n : ℕ
inst_4 : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
change : IsCyclotomicExtension.{w, z} {n} K ↥(IntermediateField.toSubalgebra K⟮ζ⟯)
⊢ IsCyclotomicExtension.{w, z} {n} K ↥K⟮ζ⟯

Tactic:
change IsCyclotomicExtension {n} K (IntermediateField.adjoin K {ζ}).toSubalgebra

Premises used: Membership.mem, Subtype, IsCyclotomicExtension, IntermediateField.adjoin, Singleton.singleton, IntermediateField.toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
n : ℕ
inst_4 : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
rw : IsCyclotomicExtension.{w, z} {n} K ↥K[ζ]
⊢ IsCyclotomicExtension.{w, z} {n} K ↥(IntermediateField.toSubalgebra K⟮ζ⟯)

Tactic:
rw [IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.isAlgebraic ζ)]

Premises used: Algebra.IsAlgebraic.isAlgebraic, IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
n : ℕ
inst_4 : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{w, z} {n} K ↥K[ζ]

Tactic:
hζ.adjoin_isCyclotomicExtension K

Premises used: Set.Mem, setOf, IsPrimitiveRoot.adjoin_isCyclotomicExtension
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsIntegral K L
n : ℕ
inst_4 : NeZero n
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{w, z} {n} K ↥K[ζ]

Tactic:
exact hζ.adjoin_isCyclotomicExtension K

Premises used: IsPrimitiveRoot.adjoin_isCyclotomicExtension
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
rw : (HPow.hPow (α := L[X]) X n - 1).Splits
⊢ Splits (map (algebraMap K L) (HPow.hPow (α := K[X]) X n - 1))

Tactic:
rw [Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X]

Premises used: Polynomial.map_one, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_sub
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
obtain : ∀ (z : L) (hz : IsPrimitiveRoot z n), (HPow.hPow (α := L[X]) X n - 1).Splits
⊢ (HPow.hPow (α := L[X]) X n - 1).Splits

Tactic:
obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)

Premises used: And.left, isCyclotomicExtension_iff, Iff.mp, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
z : L
hz : IsPrimitiveRoot z n
⊢ (HPow.hPow (α := L[X]) X n - 1).Splits

Tactic:
X_pow_sub_one_splits hz

Premises used: Polynomial.X_pow_sub_one_splits
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
H : IsCyclotomicExtension S K L
hS : n ∈ S
z : L
hz : IsPrimitiveRoot z n
⊢ (HPow.hPow (α := L[X]) X n - 1).Splits

Tactic:
exact X_pow_sub_one_splits hz

Premises used: Polynomial.X_pow_sub_one_splits
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension S K L
hS : n ∈ S
⊢ Splits (map (algebraMap K L) (cyclotomic n K))

Tactic:
(splits_X_pow_sub_one K L hS).of_dvd
    (map_ne_zero (X_pow_sub_C_ne_zero (NeZero.pos _) _)) ((map_dvd_map' _).mpr ?_)

Premises used: Iff.mpr, IsCyclotomicExtension.splits_X_pow_sub_one, NeZero.pos, Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, Polynomial.map_dvd_map', Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension S K L
hS : n ∈ S
refine : cyclotomic n K ∣ HPow.hPow (α := K[X]) X n - 1
⊢ Splits (map (algebraMap K L) (cyclotomic n K))

Tactic:
refine (splits_X_pow_sub_one K L hS).of_dvd
    (map_ne_zero (X_pow_sub_C_ne_zero (NeZero.pos _) _)) ((map_dvd_map' _).mpr ?_)

Premises used: Iff.mpr, IsCyclotomicExtension.splits_X_pow_sub_one, NeZero.pos, Polynomial.Splits.of_dvd, Polynomial.map_ne_zero, Polynomial.map_dvd_map', Polynomial.X_pow_sub_C_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension S K L
hS : n ∈ S
h : HPow.hPow (α := K[X]) X n - 1 = HMul.hMul (α := K[X]) (cyclotomic n K) (∏ i ∈ n.properDivisors, cyclotomic i K)
⊢ cyclotomic n K ∣ HPow.hPow (α := K[X]) X n - 1

Tactic:
use ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i K

Premises used: Nat.properDivisors
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension S K L
hS : n ∈ S
h h₁ : HPow.hPow (α := K[X]) X n - 1 = HPow.hPow (α := K[X]) X n - 1
⊢ HPow.hPow (α := K[X]) X n - 1 = HMul.hMul (α := K[X]) (cyclotomic n K) (∏ i ∈ n.properDivisors, cyclotomic i K)

Tactic:
rw [(eq_cyclotomic_iff (NeZero.pos _) _).1 rfl]

Premises used: Polynomial.eq_cyclotomic_iff, Iff.mp, NeZero.pos, rfl
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
⊢ Eq.{z + 1} (α := L) ((aeval b : (a : K[X]) → L) (HPow.hPow (α := K[X]) X n - 1) : L) (0 : L)

Tactic:
simp [h2]
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
⊢ IsAlgebraic K b

Tactic:
exact ⟨X ^ n - 1, (monic_X_pow_sub_C (1 : K) h1).ne_zero, by simp [h2]⟩
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
⊢ ∀ (b : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} b → IsAlgebraic K b

Tactic:
have key : ∀ b ∈ {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}, IsAlgebraic K b := by
    rintro b ⟨n, hn, h1, h2⟩
    exact ⟨X ^ n - 1, (monic_X_pow_sub_C (1 : K) h1).ne_zero, by simp [h2]⟩
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
key : ∀ (b : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} b → IsAlgebraic K b
change :
  IsCyclotomicExtension.{w, z} S K
    ↥(IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
⊢ IsCyclotomicExtension.{w, z} S K ↥(IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
change IsCyclotomicExtension S K (IntermediateField.toSubalgebra _)

Premises used: Membership.mem, Subtype, IsCyclotomicExtension, IntermediateField.toSubalgebra
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
key : ∀ (b : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} b → IsAlgebraic K b
rw : IsCyclotomicExtension.{w, z} S K ↥(adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ IsCyclotomicExtension.{w, z} S K
    ↥(IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))

Tactic:
rw [congr(IsCyclotomicExtension S K $(IntermediateField.adjoin_toSubalgebra_of_isAlgebraic key))]
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
key : ∀ (b : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} b → IsAlgebraic K b
⊢ IsCyclotomicExtension.{w, z} S K ↥(adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K L h

Premises used: Set.Mem, setOf, Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : L), IsPrimitiveRoot r n
key : ∀ (b : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} b → IsAlgebraic K b
⊢ IsCyclotomicExtension.{w, z} S K ↥(adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
exact Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S K L h

Premises used: Algebra.isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot
-- 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
⊢ Algebra.IsIntegral K L

Tactic:
have := integral S K L
-- 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
this : Algebra.IsIntegral K L
⊢ Eq.{z + 1} (α := Subalgebra K L) (adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤

Tactic:
have h := (IsCyclotomicExtension.iff_adjoin_eq_top S K L).1 ‹_› |>.2
-- 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
this : Algebra.IsIntegral K L
h : Eq.{z + 1} (α := Subalgebra K L) (adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤
⊢ Eq.{z + 1} (α := Subalgebra K L)
    (IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (IntermediateField.toSubalgebra ⊤)

Tactic:
rw [← IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
    fun b _ ↦ Algebra.IsAlgebraic.isAlgebraic b, ← IntermediateField.top_toSubalgebra] at h

Premises used: Algebra.IsAlgebraic.isAlgebraic, IntermediateField.top_toSubalgebra, IntermediateField.adjoin_toSubalgebra_of_isAlgebraic
-- 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
this : Algebra.IsIntegral K L
h :
  Eq.{z + 1} (α := Subalgebra K L)
    (IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (IntermediateField.toSubalgebra ⊤)
rw : ∀ (x : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x → IsSeparable K x
⊢ Algebra.IsSeparable K L

Tactic:
rw [← AlgEquiv.Algebra.isSeparable_iff <|
    (IntermediateField.equivOfEq (IntermediateField.toSubalgebra_injective h)).trans
      IntermediateField.topEquiv, IntermediateField.isSeparable_adjoin_iff_isSeparable]

Premises used: IntermediateField.equivOfEq, AlgEquiv.trans, IntermediateField.toSubalgebra_injective, AlgEquiv.Algebra.isSeparable_iff, IntermediateField.topEquiv, IntermediateField.isSeparable_adjoin_iff_isSeparable
-- 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
this : Algebra.IsIntegral K L
h :
  Eq.{z + 1} (α := Subalgebra K L)
    (IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (IntermediateField.toSubalgebra ⊤)
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
⊢ NeZero n

Tactic:
have := NeZero.mk h1
-- 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
this_1 : Algebra.IsIntegral K L
h :
  Eq.{z + 1} (α := Subalgebra K L)
    (IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (IntermediateField.toSubalgebra ⊤)
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
this : NeZero n
⊢ (HPow.hPow (α := K[X]) X n - 1).Separable

Tactic:
have := Polynomial.X_pow_sub_one_separable_iff.2 (neZero_of_mem' n S K L hn).out
-- 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
this_1 : Algebra.IsIntegral K L
h :
  Eq.{z + 1} (α := Subalgebra K L)
    (IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (IntermediateField.toSubalgebra ⊤)
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
this_2 : NeZero n
this : (HPow.hPow (α := K[X]) X n - 1).Separable
⊢ Eq.{z + 1} (α := L) ((aeval b : (a : K[X]) → L) (HPow.hPow (α := K[X]) X n - 1) : L) (0 : L)

Tactic:
simp [h2]
-- 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
this_1 : Algebra.IsIntegral K L
h :
  Eq.{z + 1} (α := Subalgebra K L)
    (IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (IntermediateField.toSubalgebra ⊤)
b : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : b ^ n = 1
this_2 : NeZero n
this : (HPow.hPow (α := K[X]) X n - 1).Separable
⊢ IsSeparable K b

Tactic:
exact this.of_dvd <| minpoly.dvd K b <| by simp [h2]

Premises used: minpoly.dvd, Polynomial.Separable.of_dvd
-- 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
inst_6 : IsSepClosed M
⊢ Algebra.IsSeparable K L

Tactic:
have := isSeparable S K L
-- 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
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
⊢ Nonempty (AlgEquiv.{w, z, u_1} K L ↥(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans
    (IntermediateField.equivOfEq ?_)⟩

Premises used: AlgEquiv.ofInjectiveField, IntermediateField.equivOfEq, Nonempty.intro, AlgEquiv.trans
-- 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
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
refine : i.fieldRange = IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
⊢ Nonempty (AlgEquiv.{w, z, u_1} K L ↥(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))

Tactic:
refine ⟨(show L ≃ₐ[K] i.fieldRange from AlgEquiv.ofInjectiveField i).trans
    (IntermediateField.equivOfEq ?_)⟩
-- 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
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
⊢ Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤

Tactic:
have htop : IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = ⊤ :=
    IntermediateField.adjoin_eq_top_of_algebra K _ ((iff_adjoin_eq_top S K L).1 ‹_›).2
-- 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
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
rw :
  Eq.{u_1 + 1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
⊢ i.fieldRange = IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}

Tactic:
rw [AlgHom.fieldRange_eq_map, ← htop, IntermediateField.adjoin_map]

Premises used: AlgHom.fieldRange_eq_map, IntermediateField.adjoin_map
-- 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
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
a :
  LE.le.{u_1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
a₁ :
  LE.le.{u_1} (α := IntermediateField K M) (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
⊢ Eq.{u_1 + 1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
a :
  image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} ⊆
    (↑(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) : Set M)
⊢ LE.le.{u_1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})

Tactic:
rw [IntermediateField.adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff