awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
h : IsCyclotomicExtension {n} A B
rw : Submodule.FG.{u, v} (R := A) (M := B) ⊤
rw₁ : Submodule.FG.{u, v} (R := A) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra A B) → Submodule A B) ⊤)
rw₂ rw₃ rw₄ :
  Submodule.FG.{u, v} (R := A) (M := B)
    ((Subalgebra.toSubmodule : (a : Subalgebra A B) → Submodule A B)
      (adjoin A {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}))
refine_1 : Set.Finite.{v} (α := B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ Module.Finite A B
have refine_2 : ∀ (b : B),
  Membership.mem (γ := Set B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1} b →
    ∀ (n_1 : ℕ) (hb : Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1), IsIntegral A b
Tactic: classical
  rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
  refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
  · simp only [mem_singleton_iff, exists_eq_left]
    have : {b : B | n ≠ 0 ∧ b ^ n = 1} = (nthRoots n (1 : B)).toFinset :=
      Set.ext fun x ↦ ⟨fun h ↦ by simpa [n.pos_of_neZero] using h.2,
        fun h ↦ by simpa [n.pos_of_neZero, NeZero.ne n] using h⟩
    rw [this]
    exact (nthRoots n 1).toFinset.finite_toSet
  · simp only [mem_singleton_iff] at hb
    exact ⟨X ^ n - 1,
      ⟨monic_X_pow_sub_C _ (hb.1 ▸ NeZero.ne _), by simpa [sub_eq_zero] using hb.2.2⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
h₁ : Finite (↑S : Type)
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B
have h₃ : S.Finite
Tactic: rw [finite_coe_iff] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
h₂ : IsCyclotomicExtension ∅ A B
⊢ Module.Finite A B
have empty : Eq (α := Submodule A B) (Submodule.span A (↑{1} : Set B)) ⊤
Tactic: refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
⊢ Module.Finite A B
have pos : ∀ (hn : n = 0), Module.Finite A B
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
pos : ∀ (hn : n = 0), Module.Finite A B
⊢ Module.Finite A B
have neg : ∀ (hn : ¬n = 0), Module.Finite A B
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
⊢ Module.Finite A B
have this : insert n S \ {0} = S \ {0}
Tactic: have : insert n S \ {0} = S \ {0} := by simp_all
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B
have h₃ : IsCyclotomicExtension S A B
Tactic: rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂
Cleared hypotheses: h₂, hn, this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : ¬n = 0
⊢ Module.Finite A B
have this : IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Tactic: have : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) :=
        union_left _ (insert n S) _ _ (subset_insert n S)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : ¬n = 0
this : IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Module.Finite A B
have this₁ : Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
Tactic: have := H A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1})
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : ¬n = 0
this_1 : IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this : Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B
have h₃ : IsCyclotomicExtension (S ∪ {n}) A B
Tactic: rw [← union_singleton] at h₂
Cleared hypotheses: h₂, hn, this_1, this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (S ∪ {n}) A B
hn : ¬n = 0
this_1 : IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this : Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
h_1 : IsCyclotomicExtension {n} (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B := ⋯
⊢ Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨hn⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S_1 : Set ℕ
n : ℕ
S : Set ℕ
h : n ∉ S
hs : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
h₂ : IsCyclotomicExtension (insert n S) A B
hn : ¬n = 0
this_1 : IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this : Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Module.Finite A B
have this₁ : Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B
Tactic: have : Module.Finite (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) B := by
      rw [← union_singleton] at h₂
      let _ := union_right S {n} A B
      have : NeZero n := ⟨hn⟩
      exact finite_of_singleton n _ _
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
h₁ : S.Finite
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B
have empty : ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
  [h₂ : IsCyclotomicExtension ∅ A B], Module.Finite A B
Tactic: induction S, h₁ using Set.Finite.induction_on generalizing h₂ A B with
  | empty =>
    refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
    simp [← top_toSubmodule, ← subsingleton_iff_bot_eq_top.mpr inferInstance,
      toSubmodule_bot, Submodule.one_eq_span]
  | @insert n S _ _ H =>
    by_cases hn : n = 0
    · have : insert n S \ {0} = S \ {0} := by simp_all
      rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂
      exact H A B
    have : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) :=
        union_left _ (insert n S) _ _ (subset_insert n S)
    have := H A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1})
    have : Module.Finite (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) B := by
      rw [← union_singleton] at h₂
      let _ := union_right S {n} A B
      have : NeZero n := ⟨hn⟩
      exact finite_of_singleton n _ _
    exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _
Cleared hypotheses: A, B, inst, inst_1, inst_2, inst_3, h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
h₁ : S.Finite
h₂ : IsCyclotomicExtension S A B
empty :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
    [h₂ : IsCyclotomicExtension ∅ A B], Module.Finite A B
⊢ Module.Finite A B
have insert : ∀ {n : ℕ} {S : Set ℕ},
  n ∉ S →
    S.Finite →
      ∀
        (H :
          ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
            [h₂ : IsCyclotomicExtension S A B], Module.Finite A B)
        (A : Type u) (B : Type v) [inst : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra A B] [IsDomain B]
        [h₂ : IsCyclotomicExtension (insert n S) A B], Module.Finite A B
Tactic: induction S, h₁ using Set.Finite.induction_on generalizing h₂ A B with
  | empty =>
    refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
    simp [← top_toSubmodule, ← subsingleton_iff_bot_eq_top.mpr inferInstance,
      toSubmodule_bot, Submodule.one_eq_span]
  | @insert n S _ _ H =>
    by_cases hn : n = 0
    · have : insert n S \ {0} = S \ {0} := by simp_all
      rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂
      exact H A B
    have : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) :=
        union_left _ (insert n S) _ _ (subset_insert n S)
    have := H A (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1})
    have : Module.Finite (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) B := by
      rw [← union_singleton] at h₂
      let _ := union_right S {n} A B
      have : NeZero n := ⟨hn⟩
      exact finite_of_singleton n _ _
    exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _
Cleared hypotheses: A, B, inst, inst_1, inst_2, inst_3, h₁, h₂
-- 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 : NumberField K
inst_3 : Finite (↑S : Type)
inst_4 : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L
have this : CharZero L
Tactic: haveI := charZero_of_injective_algebraMap (algebraMap K L).injective
-- 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 : NumberField K
inst_3 : Finite (↑S : Type)
inst_4 : IsCyclotomicExtension S K L
this : CharZero L
⊢ FiniteDimensional ℚ L
have this₁ : Module.Finite K L
Tactic: haveI := IsCyclotomicExtension.finite S K L
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B))
    (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
have simp : Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})
Tactic: simp only [mem_singleton_iff, exists_eq_left]
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})
have refine_1 : ∀ (x : B) (hx : x ∈ rootSet (cyclotomic n A) B), Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x
Tactic: refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
refine_1 : ∀ (x : B) (hx : x ∈ rootSet (cyclotomic n A) B), Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})
have refine_2 : ∀ (x : B) (hx : Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x),
  x ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)
Tactic: refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
⊢ Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x
have hx₁ : Ne (α := B[X]) (map (algebraMap A B) (cyclotomic n A)) 0 ∧
  Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
Tactic: rw [mem_rootSet'] at hx
Cleared hypotheses: hx
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx :
  Ne (α := B[X]) (map (algebraMap A B) (cyclotomic n A)) 0 ∧
    Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
⊢ n ≠ 0 ∧ x ^ n = 1
have refine_1 : n ≠ 0 ∧ ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x
Tactic: rw [isRoot_of_unity_iff (NeZero.pos n)]
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx :
  Ne (α := B[X]) (map (algebraMap A B) (cyclotomic n A)) 0 ∧
    Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
⊢ n ≠ 0 ∧ ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x
have refine_1 : IsRoot (cyclotomic n B) x
Tactic: refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx :
  Ne (α := B[X]) (map (algebraMap A B) (cyclotomic n A)) 0 ∧
    Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
⊢ IsRoot (cyclotomic n B) x
have refine_1 : Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
Tactic: rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map_algebraMap]
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
x : B
hx : n ≠ 0 ∧ x ^ n = 1
⊢ x ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)
have refine_2 : ∀ i < n, ∀ (hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1), ζ ^ i ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)
Tactic: obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2
Cleared hypotheses: x, hx
-- 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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ^ i ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)
have refine_2 : ζ ∈ rootSet (cyclotomic n A) B
Tactic: refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (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
inst_3 : IsDomain B
ζ : B
n : ℕ
inst_4 : NeZero n
hζ : IsPrimitiveRoot ζ n
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ∈ rootSet (cyclotomic n A) B
have refine_2 : Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) ζ
Tactic: rw [mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, map_cyclotomic, ← IsRoot]
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) A[ζ]
have refine_1 : ∀ (x : B) (hx : x ∈ rootSet (cyclotomic n A) B), x ∈ (↑A[ζ] : Set B)
Tactic: refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
refine_1 : ∀ (x : B) (hx : x ∈ rootSet (cyclotomic n A) B), x ∈ (↑A[ζ] : Set B)
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) A[ζ]
have refine_2 : ∀ (x : B) (hx : Membership.mem (γ := Set B) {ζ} x), x ∈ rootSet (cyclotomic n A) B
Tactic: refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono fun x hx => ?_)
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx_1 : x ∈ rootSet (cyclotomic n A) B
hx : x ^ n = 1
⊢ x ∈ (↑A[ζ] : Set B)
have obtain : ∀ i < n, ∀ (hx : ζ ^ i ∈ rootSet (cyclotomic n A) B) (hx : (ζ ^ i) ^ n = 1), ζ ^ i ∈ (↑A[ζ] : Set B)
Tactic: obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
Cleared hypotheses: x, hx_1, hx
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
⊢ x ∈ (↑A[ζ] : Set B)
have refine_1 : x ^ n = 1
Tactic: suffices hx : x ^ n = 1 by
      obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
      exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
⊢ x ^ n = 1
have refine_1 : ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x
Tactic: refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
⊢ ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x
have refine_1 : IsRoot (cyclotomic n B) x
Tactic: refine ⟨n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
⊢ IsRoot (cyclotomic n B) x
have hx₁ : Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) x
Tactic: rw [mem_rootSet', ← eval_map_algebraMap, map_cyclotomic, ← IsRoot] at hx
Cleared hypotheses: hx
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : Membership.mem (γ := Set B) {ζ} x
⊢ x ∈ rootSet (cyclotomic n A) B
have hx₁ : x = ζ
Tactic: simp only [mem_singleton_iff] at hx
Cleared hypotheses: hx
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) A[ζ] ⊤
have rw : Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) ⊤
Tactic: rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) ⊤
have rw : Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1}) ⊤
Tactic: rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) A[ζ] ⊤
have rw : Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) ⊤
Tactic: classical
  rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
  rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
  exact ((iff_adjoin_eq_top {n} A B).mp h).2
-- 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
rw rw₁ rw₂ : Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) ⊤
⊢ Eq (α := Subalgebra A B) A[ζ] ⊤
have rw₃ : Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1}) ⊤
Tactic: classical
  rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]
  rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]
  exact ((iff_adjoin_eq_top {n} A B).mp h).2