awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
n_1 : ℕ
hi : Membership.mem (γ := Set ℕ) {n} n_1
hi' : n_1 ≠ 0
⊢ ∃ (r : ↥A[ζ]), IsPrimitiveRoot r n_1
have hi₁ : n_1 = n
Tactic: rw [Set.mem_singleton_iff] at hi
Cleared hypotheses: hi, hi'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
n_1 : ℕ
hi : n_1 = n
hi' : n_1 ≠ 0
⊢ ∃ (r : ↥A[ζ]), IsPrimitiveRoot r n_1
have refine : IsPrimitiveRoot (M := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ sorry) n_1
Tactic: refine ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
n_1 : ℕ
hi : n_1 = n
hi' : n_1 ≠ 0
⊢ IsPrimitiveRoot (M := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n_1
have rwa : IsPrimitiveRoot (↑(Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ sorry) : B) n_1
Tactic: rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
n_1 : ℕ
hi : n_1 = n
hi' : n_1 ≠ 0
rwa : IsPrimitiveRoot (↑(Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) : B) n_1
⊢ IsPrimitiveRoot (M := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n_1
have rwa₁ : IsPrimitiveRoot ζ n_1
Tactic: rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ 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) x hx)
have refine_1 : ∀ (b : B) (hb : Membership.mem (γ := Set B) {ζ} b),
  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 sorry)
Tactic: refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
refine_1 :
  ∀ (b : B) (hb : Membership.mem (γ := Set B) {ζ} b),
    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 ⋯)
⊢ 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) x hx)
have refine_2 : ∀ (a : A),
  Membership.mem.{v, v} (α := ↥A[ζ]) (γ := 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) ((algebraMap A B : (a : A) → B) a) sorry :
      ↥A[ζ])
Tactic: refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
refine_1 :
  ∀ (b : B) (hb : Membership.mem (γ := Set B) {ζ} b),
    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 ⋯)
refine_2 :
  ∀ (a : A),
    Membership.mem.{v, v} (α := ↥A[ζ]) (γ := 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) ((algebraMap A B : (a : A) → B) a)
          ⋯ :
        ↥A[ζ])
⊢ 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) x hx)
have refine_3 : ∀ (b₁ b₂ : B) (x : Membership.mem (γ := Subalgebra A B) A[ζ] b₁) (x_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₁ x))
  (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₂ x_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₂) sorry)
Tactic: refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
refine_1 :
  ∀ (b : B) (hb : Membership.mem (γ := Set B) {ζ} b),
    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 ⋯)
refine_2 :
  ∀ (a : A),
    Membership.mem.{v, v} (α := ↥A[ζ]) (γ := 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) ((algebraMap A B : (a : A) → B) a)
          ⋯ :
        ↥A[ζ])
refine_3 :
  ∀ (b₁ b₂ : B) (x : Membership.mem (γ := Subalgebra A B) A[ζ] b₁) (x_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₁ x))
    (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₂ x_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₂) ⋯)
⊢ 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) x hx)
have refine_4 : ∀ (b₁ b₂ : B) (x : Membership.mem (γ := Subalgebra A B) A[ζ] b₁) (x_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₁ x))
  (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₂ x_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₂) sorry)
Tactic: refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
hb : Membership.mem (γ := Set B) {ζ} b
⊢ 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 ⋯)
have hb₁ : b = ζ
Tactic: rw [Set.mem_singleton_iff] at hb
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
⊢ 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 ⋯)
have refine_1 : Membership.mem (γ := Set ↥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 sorry)
Tactic: refine subset_adjoin ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
⊢ Membership.mem (γ := Set ↥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 ⋯)
have refine_1 : n ≠ 0 ∧ HPow.hPow (α := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ sorry) n = 1
Tactic: simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq, hb]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
⊢ n ≠ 0 ∧ HPow.hPow (α := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n = 1
have refine_1 : n ≠ 0 ∧ ζ ^ n = 1
Tactic: rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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⟮ζ⟯
have change : IsCyclotomicExtension.{w, z} {n} K ↥(IntermediateField.toSubalgebra K⟮ζ⟯)
Tactic: change IsCyclotomicExtension {n} K (IntermediateField.adjoin K {ζ}).toSubalgebra
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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 ↥(IntermediateField.toSubalgebra K⟮ζ⟯)
have rw : IsCyclotomicExtension.{w, z} {n} K ↥K[ζ]
Tactic: rw [IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic (IsAlgebraic.isAlgebraic ζ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ Splits (map (algebraMap K L) (HPow.hPow (α := K[X]) X n - 1))
have rw : (HPow.hPow (α := L[X]) X n - 1).Splits
Tactic: rw [Polynomial.map_sub, Polynomial.map_one, Polynomial.map_pow,
    Polynomial.map_X]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ (HPow.hPow (α := L[X]) X n - 1).Splits
have obtain : ∀ (z : L) (hz : IsPrimitiveRoot z n), (HPow.hPow (α := L[X]) X n - 1).Splits
Tactic: obtain ⟨z, hz⟩ := ((isCyclotomicExtension_iff _ _ _).1 H).1 hS (NeZero.ne _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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))
have refine : cyclotomic n K ∣ HPow.hPow (α := K[X]) X n - 1
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 ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ cyclotomic n K ∣ HPow.hPow (α := K[X]) X n - 1
have h : HPow.hPow (α := K[X]) X n - 1 = HMul.hMul (α := K[X]) (cyclotomic n K) (∏ i ∈ n.properDivisors, cyclotomic i K)
Tactic: use ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i K
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ HPow.hPow (α := K[X]) X n - 1 = HMul.hMul (α := K[X]) (cyclotomic n K) (∏ i ∈ n.properDivisors, cyclotomic i K)
have h : HPow.hPow (α := K[X]) X n - 1 = HPow.hPow (α := K[X]) X n - 1
Tactic: rw [(eq_cyclotomic_iff (NeZero.pos _) _).1 rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
⊢ IsCyclotomicExtension.{w, z} S K ↥(IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
have key : ∀ (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]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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 ↥(IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
have change : IsCyclotomicExtension.{w, z} S K
  ↥(IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
Tactic: change IsCyclotomicExtension S K (IntermediateField.toSubalgebra _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
    ↥(IntermediateField.toSubalgebra (IntermediateField.adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
have rw : IsCyclotomicExtension.{w, z} S K ↥(adjoin K {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Tactic: rw [congr(IsCyclotomicExtension S K $(IntermediateField.adjoin_toSubalgebra_of_isAlgebraic key))]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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.IsSeparable K L
have this : Algebra.IsIntegral K L
Tactic: have := integral S K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
⊢ Algebra.IsSeparable K L
have h : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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}) ⊤
⊢ Algebra.IsSeparable K L
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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 ⊤)
⊢ Algebra.IsSeparable K L
have rw : ∀ (x : L), Membership.mem (γ := Set L) {b : L | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x → IsSeparable K x
Tactic: rw [← AlgEquiv.Algebra.isSeparable_iff <|
    (IntermediateField.equivOfEq (IntermediateField.toSubalgebra_injective h)).trans
      IntermediateField.topEquiv, IntermediateField.isSeparable_adjoin_iff_isSeparable]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
⊢ IsSeparable K b
have this₁ : NeZero n
Tactic: have := NeZero.mk h1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
⊢ IsSeparable K b
have this₁ : (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
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
⊢ Nonempty (AlgEquiv.{w, z, u_1} K L ↥(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
have this : Algebra.IsSeparable K L
Tactic: have := isSeparable S K L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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}))
have refine : i.fieldRange = 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 ?_)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
⊢ i.fieldRange = IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
have htop : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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}) ⊤
⊢ i.fieldRange = IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
have 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})
Tactic: rw [AlgHom.fieldRange_eq_map, ← htop, IntermediateField.adjoin_map]