awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
x y : B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
r : B
hr1 : IsPrimitiveRoot r n
hr2 : Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
this : NeZero n
⊢ Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
have h : ∀ (m : ℕ) (h2 : (r ^ m) ^ n = 1), Eq (α := B) ((f : (a : B) → B) (r ^ m) : B) ((g : (a : B) → B) (r ^ m) : B)
Tactic: obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
Cleared hypotheses: y, h2
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
x : B
hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
⊢ Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B)
have h : ∀ (y : B) (hy : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} y),
  Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
Tactic: induction hx using Algebra.adjoin_induction with
  | mem y hy =>
    obtain ⟨n, hn, h1, h2⟩ := hy
    obtain ⟨r, hr1, hr2⟩ := H n hn h1
    have := NeZero.mk h1
    obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
    simp [hr2]
  | algebraMap y => simp
  | add x y hx hy ihx ihy => simp [ihx, ihy]
  | mul x y hx hy ihx ihy => simp [ihx, ihy]
Cleared hypotheses: hx
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
x : B
hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
h :
  ∀ (y : B) (hy : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} y),
    Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
⊢ Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B)
have h₁ : ∀ (y : A),
  Eq (α := B) ((f : (a : B) → B) ((algebraMap A B : (a : A) → B) y : B) : B)
    ((g : (a : B) → B) ((algebraMap A B : (a : A) → B) y : B) : B)
Tactic: induction hx using Algebra.adjoin_induction with
  | mem y hy =>
    obtain ⟨n, hn, h1, h2⟩ := hy
    obtain ⟨r, hr1, hr2⟩ := H n hn h1
    have := NeZero.mk h1
    obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
    simp [hr2]
  | algebraMap y => simp
  | add x y hx hy ihx ihy => simp [ihx, ihy]
  | mul x y hx hy ihx ihy => simp [ihx, ihy]
Cleared hypotheses: hx
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
x : B
hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
h :
  ∀ (y : B) (hy : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} y),
    Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
h₁ :
  ∀ (y : A),
    Eq (α := B) ((f : (a : B) → B) ((algebraMap A B : (a : A) → B) y : B) : B)
      ((g : (a : B) → B) ((algebraMap A B : (a : A) → B) y : B) : B)
⊢ Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B)
have h₂ : ∀ (x y : B) (hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
  (hy : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) y)
  (ihx : Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B))
  (ihy : Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)),
  Eq (α := B) ((f : (a : B) → B) (x + y) : B) ((g : (a : B) → B) (x + y) : B)
Tactic: induction hx using Algebra.adjoin_induction with
  | mem y hy =>
    obtain ⟨n, hn, h1, h2⟩ := hy
    obtain ⟨r, hr1, hr2⟩ := H n hn h1
    have := NeZero.mk h1
    obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
    simp [hr2]
  | algebraMap y => simp
  | add x y hx hy ihx ihy => simp [ihx, ihy]
  | mul x y hx hy ihx ihy => simp [ihx, ihy]
Cleared hypotheses: hx
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
H : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
x : B
hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
h :
  ∀ (y : B) (hy : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} y),
    Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
h₁ :
  ∀ (y : A),
    Eq (α := B) ((f : (a : B) → B) ((algebraMap A B : (a : A) → B) y : B) : B)
      ((g : (a : B) → B) ((algebraMap A B : (a : A) → B) y : B) : B)
h₂ :
  ∀ (x y : B) (hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
    (hy : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) y)
    (ihx : Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B))
    (ihy : Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)),
    Eq (α := B) ((f : (a : B) → B) (x + y) : B) ((g : (a : B) → B) (x + y) : B)
⊢ Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B)
have h₃ : ∀ (x y : B) (hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
  (hy : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) y)
  (ihx : Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B))
  (ihy : Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)),
  Eq (α := B) ((f : (a : B) → B) (x * y) : B) ((g : (a : B) → B) (x * y) : B)
Tactic: induction hx using Algebra.adjoin_induction with
  | mem y hy =>
    obtain ⟨n, hn, h1, h2⟩ := hy
    obtain ⟨r, hr1, hr2⟩ := H n hn h1
    have := NeZero.mk h1
    obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2
    simp [hr2]
  | algebraMap y => simp
  | add x y hx hy ihx ihy => simp [ihx, ihy]
  | mul x y hx hy ihx ihy => simp [ihx, ihy]
Cleared hypotheses: hx
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
⊢ IsMulCommutative.{v} (B ≃ₐ[A] B)
have refine : ∀ (f g : B ≃ₐ[A] B) (n : ℕ) (hn : n ∈ S) (h1 : n ≠ 0),
  ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
Tactic: refine ⟨⟨fun f g ↦ algEquiv_eq_of_apply_eq S A B fun n hn h1 ↦ ?_⟩⟩
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
⊢ ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
have obtain : ∀ (r : B) (hr : IsPrimitiveRoot r n),
  ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
Tactic: obtain ⟨r, hr⟩ := ‹IsCyclotomicExtension S A B›.exists_isPrimitiveRoot hn h1
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
⊢ ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
have right : Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
Tactic: use r, hr
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
⊢ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
have right : Eq (α := B) ((f : (a : B) → B) ((g : (a : B) → B) r : B) : B) ((g : (a : B) → B) ((f : (a : B) → B) r : B) : B)
Tactic: simp only [AlgEquiv.mul_apply]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
⊢ Eq (α := B) ((f : (a : B) → B) ((g : (a : B) → B) r : B) : B) ((g : (a : B) → B) ((f : (a : B) → B) r : B) : B)
have this : NeZero n
Tactic: have := NeZero.mk h1
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
⊢ HPow.hPow (α := B) ((f : (a : B) → B) r : B) n = 1
have rw : Eq (α := B) ((f : (a : B) → B) (r ^ n) : B) (1 : B)
Tactic: rw [← map_pow, hr.1, map_one]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
rw : Eq (α := B) ((f : (a : B) → B) (r ^ n) : B) (1 : B)
⊢ HPow.hPow (α := B) ((f : (a : B) → B) r : B) n = 1
have rw₁ : Eq (α := B) ((f : (a : B) → B) 1 : B) (1 : B)
Tactic: rw [← map_pow, hr.1, map_one]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
rw : Eq (α := B) ((f : (a : B) → B) (r ^ n) : B) (1 : B)
rw₁ : Eq (α := B) ((f : (a : B) → B) 1 : B) (1 : B)
⊢ HPow.hPow (α := B) ((f : (a : B) → B) r : B) n = 1
have rw₂ : Eq.{v + 1} (α := B) 1 1
Tactic: rw [← map_pow, hr.1, map_one]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
⊢ Eq (α := B) ((f : (a : B) → B) ((g : (a : B) → B) r : B) : B) ((g : (a : B) → B) ((f : (a : B) → B) r : B) : B)
have right : ∀ (mf : ℕ) (hf : r ^ mf = (f : (a : B) → B) r),
  Eq (α := B) ((f : (a : B) → B) ((g : (a : B) → B) r : B) : B) ((g : (a : B) → B) ((f : (a : B) → B) r : B) : B)
Tactic: obtain ⟨mf, -, hf⟩ := hr.eq_pow_of_pow_eq_one (show f r ^ n = 1 by rw [← map_pow, hr.1, map_one])
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
mf : ℕ
hf : r ^ mf = (f : (a : B) → B) r
⊢ HPow.hPow (α := B) ((g : (a : B) → B) r : B) n = 1
have rw : Eq (α := B) ((g : (a : B) → B) (r ^ n) : B) (1 : B)
Tactic: rw [← map_pow, hr.1, map_one]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
mf : ℕ
hf : r ^ mf = (f : (a : B) → B) r
rw : Eq (α := B) ((g : (a : B) → B) (r ^ n) : B) (1 : B)
⊢ HPow.hPow (α := B) ((g : (a : B) → B) r : B) n = 1
have rw₁ : Eq (α := B) ((g : (a : B) → B) 1 : B) (1 : B)
Tactic: rw [← map_pow, hr.1, map_one]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
mf : ℕ
hf : r ^ mf = (f : (a : B) → B) r
rw : Eq (α := B) ((g : (a : B) → B) (r ^ n) : B) (1 : B)
rw₁ : Eq (α := B) ((g : (a : B) → B) 1 : B) (1 : B)
⊢ HPow.hPow (α := B) ((g : (a : B) → B) r : B) n = 1
have rw₂ : Eq.{v + 1} (α := B) 1 1
Tactic: rw [← map_pow, hr.1, map_one]
-- 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 : IsCyclotomicExtension S A B
inst_4 : IsDomain B
f g : B ≃ₐ[A] B
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr : IsPrimitiveRoot r n
this : NeZero n
mf : ℕ
hf : r ^ mf = (f : (a : B) → B) r
⊢ Eq (α := B) ((f : (a : B) → B) ((g : (a : B) → B) r : B) : B) ((g : (a : B) → B) ((f : (a : B) → B) r : B) : B)
have right : ∀ (mg : ℕ) (hg : r ^ mg = (g : (a : B) → B) r),
  Eq (α := B) ((f : (a : B) → B) ((g : (a : B) → B) r : B) : B) ((g : (a : B) → B) ((f : (a : B) → B) r : B) : B)
Tactic: obtain ⟨mg, -, hg⟩ := hr.eq_pow_of_pow_eq_one (show g r ^ n = 1 by rw [← map_pow, hr.1, map_one])
-- 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
⊢ Module.Finite A B
have 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}))
Tactic: rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]
-- 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
⊢ 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}))
have refine_1 : Set.Finite.{v} (α := B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
Tactic: refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
-- 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
refine_1 : Set.Finite.{v} (α := B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
⊢ 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}))
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: refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
-- 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
⊢ Set.Finite.{v} (α := B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
have refine_1 : Set.Finite.{v} (α := B) {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 (hypothesis)
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
⊢ Set.Finite.{v} (α := B) {b : B | n ≠ 0 ∧ b ^ n = 1}
have this : {b : B | n ≠ 0 ∧ b ^ n = 1} = (↑(Multiset.toFinset (nthRoots n 1)) : Set B)
Tactic: 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⟩
-- 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
this : {b : B | n ≠ 0 ∧ b ^ n = 1} = (↑(Multiset.toFinset (nthRoots n 1)) : Set B)
⊢ Set.Finite.{v} (α := B) {b : B | n ≠ 0 ∧ b ^ n = 1}
have refine_1 : (↑(Multiset.toFinset (nthRoots n 1)) : Set B).Finite
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n_1 : ℕ
inst : NeZero n_1
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_1} A B
b : B
h_1 : Membership.mem (γ := Set B) {b : B | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {n_1} n ∧ n ≠ 0 ∧ b ^ n = 1} b
n : ℕ
hb : Membership.mem (γ := Set ℕ) {n_1} n ∧ n ≠ 0 ∧ b ^ n = 1
⊢ IsIntegral A b
have hb₁ : n = n_1 ∧ n ≠ 0 ∧ b ^ n = 1
Tactic: simp only [mem_singleton_iff] at hb
Cleared hypotheses: hb
-- 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
⊢ Module.Finite A B
have rw : Submodule.FG.{u, v} (R := A) (M := 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 (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) ⊤
⊢ Module.Finite A B
have rw₁ : Submodule.FG.{u, v} (R := A) (M := B) ((Subalgebra.toSubmodule : (a : Subalgebra A B) → Submodule 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 (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) ⊤)
⊢ Module.Finite A B
have 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}))
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 (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}))
⊢ Module.Finite A B
have refine_1 : Set.Finite.{v} (α := B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
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⟩⟩