awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
hy : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} y
h :
  ∀ (n : ℕ) (hn : n ∈ S) (h1 : n ≠ 0) (h2 : y ^ n = 1), Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
⊢ Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)

Tactic:
obtain ⟨n, hn, h1, h2⟩ := hy
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
h :
  ∀ (r : B) (hr1 : IsPrimitiveRoot r n) (hr2 : Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)),
    Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)
⊢ Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)

Tactic:
obtain ⟨r, hr1, hr2⟩ := H n hn h1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
⊢ NeZero n

Tactic:
have := NeZero.mk h1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
h : ∀ (m : ℕ) (h2 : (r ^ m) ^ n = 1), Eq (α := B) ((f : (a : B) → B) (r ^ m) : B) ((g : (a : B) → B) (r ^ m) : B)
⊢ Eq (α := B) ((f : (a : B) → B) y : B) ((g : (a : B) → B) y : B)

Tactic:
obtain ⟨m, -, rfl⟩ := hr1.eq_pow_of_pow_eq_one h2

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
r : B
hr1 : IsPrimitiveRoot r n
hr2 : Eq (α := B) ((f : (a : B) → B) r : B) ((g : (a : B) → B) r : B)
this : NeZero n
m : ℕ
h2 : (r ^ m) ^ n = 1
⊢ Eq (α := B) ((f : (a : B) → B) (r ^ m) : B) ((g : (a : B) → B) (r ^ m) : B)

Tactic:
simp [hr2]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 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:
simp [ihx, ihy]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 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:
simp [ihx, ihy]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
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)

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]

Premises used: Algebra.algebraMap, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)

Tactic:
⟨⟨fun f g ↦ algEquiv_eq_of_apply_eq S A B fun n hn h1 ↦ ?_⟩⟩

Premises used: IsCyclotomicExtension.algEquiv_eq_of_apply_eq, IsMulCommutative.mk, Std.Commutative.mk
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ IsMulCommutative.{v} (B ≃ₐ[A] B)

Tactic:
refine ⟨⟨fun f g ↦ algEquiv_eq_of_apply_eq S A B fun n hn h1 ↦ ?_⟩⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ ∃ (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

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
right : Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)
⊢ ∃ (r : B), IsPrimitiveRoot r n ∧ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)

Tactic:
use r, hr
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ Eq (α := B) ((f * g : (a : B) → B) r : B) ((g * f : (a : B) → B) r : B)

Tactic:
simp only [AlgEquiv.mul_apply]

Premises used: AlgEquiv.mul_apply
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ NeZero n

Tactic:
have := NeZero.mk h1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
rw₂ rw₃ : Eq.{v + 1} (α := B) 1 1
⊢ HPow.hPow (α := B) ((f : (a : B) → B) r : B) n = 1

Tactic:
rw [← map_pow, hr.1, map_one]

Premises used: map_pow, map_one, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ 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])

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
rw₂ rw₃ : Eq.{v + 1} (α := B) 1 1
⊢ HPow.hPow (α := B) ((g : (a : B) → B) r : B) n = 1

Tactic:
rw [← map_pow, hr.1, map_one]

Premises used: map_pow, map_one, IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ 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])

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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:
simp [← hf, ← hg, ← pow_mul, mul_comm mf mg]

Premises used: pow_mul, mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
    ((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

Tactic:
rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]

Premises used: Algebra.top_toSubmodule, Module.finite_def, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}))

Tactic:
fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_

Premises used: _private.0.IsCyclotomicExtension.finite_of_singleton.match_1, IsIntegral, fg_adjoin_of_finite
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}
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
⊢ 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:
refine fg_adjoin_of_finite ?_ fun b ⟨n, hb⟩ => ?_
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 ≠ 0 ∧ b ^ n = 1}
⊢ Set.Finite.{v} (α := B) {b : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}

Tactic:
simp only [mem_singleton_iff, exists_eq_left]

Premises used: exists_eq_left, Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 : IsCyclotomicExtension {n} A B
x : B
h : Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x
⊢ x ∈ (↑(Multiset.toFinset (nthRoots n 1)) : Set B)

Tactic:
simpa [n.pos_of_neZero] using h.2

Premises used: And.right, Nat.pos_of_neZero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 : IsCyclotomicExtension {n} A B
x : B
h : x ∈ (↑(Multiset.toFinset (nthRoots n 1)) : Set B)
⊢ Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x

Tactic:
simpa [n.pos_of_neZero, NeZero.ne n] using h

Premises used: Nat.pos_of_neZero, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ {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⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
refine_1 : (↑(Multiset.toFinset (nthRoots n 1)) : Set B).Finite
⊢ Set.Finite.{v} (α := B) {b : B | n ≠ 0 ∧ b ^ n = 1}

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
⊢ (↑(Multiset.toFinset (nthRoots n 1)) : Set B).Finite

Tactic:
(nthRoots n 1).toFinset.finite_toSet

Premises used: Multiset.toFinset, Polynomial.nthRoots, Finset.finite_toSet, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
⊢ (↑(Multiset.toFinset (nthRoots n 1)) : Set B).Finite

Tactic:
exact (nthRoots n 1).toFinset.finite_toSet

Premises used: Multiset.toFinset, Polynomial.nthRoots, Finset.finite_toSet, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ n = n_1 ∧ n ≠ 0 ∧ b ^ n = 1

Tactic:
simp only [mem_singleton_iff] at hb

Premises used: Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 : n = n_1 ∧ n ≠ 0 ∧ b ^ n = 1
⊢ eval₂ (algebraMap A B) b (HPow.hPow (α := A[X]) X n - 1) = 0

Tactic:
simpa [sub_eq_zero] using hb.2.2

Premises used: sub_eq_zero, And.right
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 : n = n_1 ∧ n ≠ 0 ∧ b ^ n = 1
⊢ IsIntegral A b

Tactic:
exact ⟨X ^ n - 1,
      ⟨monic_X_pow_sub_C _ (hb.1 ▸ NeZero.ne _), by simpa [sub_eq_zero] using hb.2.2⟩⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}
refine_2 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
⊢ Module.Finite 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⟩⟩

Premises used: Multiset.toFinset, Algebra.top_toSubmodule, exists_eq_left, Polynomial.nthRoots, Set.mem_singleton_iff, Module.finite_def, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Finset.finite_toSet, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ S.Finite

Tactic:
rw [finite_coe_iff] at h₁

Premises used: Set.finite_coe_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
h₃ : S.Finite
⊢ IsCyclotomicExtension S A B

Tactic:
rw [finite_coe_iff] at h₁

Premises used: Set.finite_coe_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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

Tactic:
Module.finite_def.2 ⟨({1} : Finset B), ?_⟩

Premises used: Iff.mpr, Module.finite_def, Exists.intro, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
empty : Eq (α := Submodule A B) (Submodule.span A (↑{1} : Set B)) ⊤
⊢ Module.Finite A B

Tactic:
refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩

Premises used: Iff.mpr, Module.finite_def, Exists.intro, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ Eq (α := Submodule A B) (Submodule.span A (↑{1} : Set B)) ⊤

Tactic:
simp [← top_toSubmodule, ← subsingleton_iff_bot_eq_top.mpr inferInstance,
      toSubmodule_bot, Submodule.one_eq_span]

Premises used: Iff.mpr, Algebra.toSubmodule_bot, Algebra.top_toSubmodule, inferInstance, subsingleton_iff_bot_eq_top, Submodule.one_eq_span