awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
neg : ∀ (hn : ¬n = 0), Module.Finite A B
⊢ Module.Finite A B

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ insert n S \ {0} = S \ {0}

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ insert n S \ {0} = S \ {0}

Tactic:
have : insert n S \ {0} = S \ {0} := by simp_all
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}
⊢ IsCyclotomicExtension S A B

Tactic:
rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂

Premises used: IsCyclotomicExtension.eq_self_sdiff_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}
h₃ : IsCyclotomicExtension S A B
⊢ n = 0

Tactic:
rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂

Premises used: IsCyclotomicExtension.eq_self_sdiff_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}
h₃ : IsCyclotomicExtension S A B
hn₁ : n = 0
⊢ insert n S \ {0} = S \ {0}

Tactic:
rw [eq_self_sdiff_zero, this, ← eq_self_sdiff_zero] at h₂

Premises used: IsCyclotomicExtension.eq_self_sdiff_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B

Tactic:
H A B
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 A B
hn : n = 0
this : insert n S \ {0} = S \ {0}
⊢ Module.Finite A B

Tactic:
exact H A B
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ 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)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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.{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})
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
⊢ IsCyclotomicExtension (S ∪ {n}) A B

Tactic:
rw [← union_singleton] at h₂

Premises used: Set.union_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
h₃ : IsCyclotomicExtension (S ∪ {n}) A B
⊢ ¬n = 0

Tactic:
rw [← union_singleton] at h₂

Premises used: Set.union_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
h₃ : IsCyclotomicExtension (S ∪ {n}) A B
hn₁ : ¬n = 0
⊢ IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
rw [← union_singleton] at h₂

Premises used: Set.union_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
h₃ : IsCyclotomicExtension (S ∪ {n}) A B
hn₁ : ¬n = 0
this₁ : IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
rw [← union_singleton] at h₂

Premises used: Set.union_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 := ⋯
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_2 : 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 := ⋯
this : NeZero n
⊢ Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B

Tactic:
finite_of_singleton n _ _

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, IsCyclotomicExtension.finite_of_singleton, Algebra.adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_2 : 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 := ⋯
this : NeZero n
⊢ Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B

Tactic:
exact finite_of_singleton n _ _

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

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 _ _
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_2 : Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this : Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B
⊢ Module.Finite A B

Tactic:
Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _

Premises used: setOf, Algebra.adjoin, Membership.mem, Exists, Subtype, Ne, And, HPow.hPow, Module.Finite.trans, OfNat.ofNat, Eq
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_2 : Module.Finite.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
this : Module.Finite (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B
⊢ Module.Finite A B

Tactic:
exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1}) _

Premises used: setOf, Algebra.adjoin, Membership.mem, Exists, Subtype, Ne, And, HPow.hPow, Module.Finite.trans, OfNat.ofNat, Eq
-- 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₁ : 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
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.insert n S) A B], Module.Finite 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}) _

Premises used: Iff.mpr, Algebra.toSubmodule_bot, setOf, Algebra.adjoin, Algebra.top_toSubmodule, Membership.mem, Exists, inferInstance, Subtype, Insert.insert, Ne, And, Module.finite_def, HPow.hPow, Module.Finite.trans, Exists.intro, IsCyclotomicExtension.eq_self_sdiff_zero, subsingleton_iff_bot_eq_top, Singleton.singleton, OfNat.ofNat, Eq, Submodule.one_eq_span
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
h : NumberField K
inst_3 : Finite (↑S : Type)
inst_4 : IsCyclotomicExtension S K L
⊢ CharZero L

Tactic:
haveI := charZero_of_injective_algebraMap (algebraMap K L).injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
h : NumberField K
inst_3 : Finite (↑S : Type)
inst_4 : IsCyclotomicExtension S K L
this : CharZero L
⊢ Module.Finite K L

Tactic:
haveI := IsCyclotomicExtension.finite S K L
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
h : NumberField K
inst_3 : Finite (↑S : Type)
inst_4 : IsCyclotomicExtension S K L
this_1 : CharZero L
this : Module.Finite K L
⊢ FiniteDimensional ℚ L

Tactic:
Module.Finite.trans K _

Premises used: Module.Finite.trans
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
h : NumberField K
inst_3 : Finite (↑S : Type)
inst_4 : IsCyclotomicExtension S K L
this_1 : CharZero L
this : Module.Finite K L
⊢ FiniteDimensional ℚ L

Tactic:
exact Module.Finite.trans K _

Premises used: Module.Finite.trans
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
inst : Field K
C : Type z
inst_1 : Finite (↑S : Type)
inst_2 : CommRing C
inst_3 : Algebra K C
inst_4 : IsDomain C
inst_5 : IsCyclotomicExtension S K C
⊢ FiniteDimensional K C

Tactic:
IsCyclotomicExtension.finite S K C

Premises used: IsCyclotomicExtension.finite
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
simp : Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})
⊢ 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})

Tactic:
simp only [mem_singleton_iff, exists_eq_left]

Premises used: exists_eq_left, Set.mem_singleton_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})

Tactic:
le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)

Premises used: le_antisymm, Algebra.adjoin_mono, Algebra.adjoin_le
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})

Tactic:
refine le_antisymm (adjoin_mono fun x hx => ?_) (adjoin_le fun x hx => ?_)

Premises used: le_antisymm, Algebra.adjoin_mono, Algebra.adjoin_le
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ 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

Premises used: Polynomial.mem_rootSet'
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
refine_1 : n ≠ 0 ∧ ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x
⊢ n ≠ 0 ∧ x ^ n = 1

Tactic:
rw [isRoot_of_unity_iff (NeZero.pos n)]

Premises used: NeZero.pos, isRoot_of_unity_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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

Tactic:
⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩

Premises used: And.intro, Exists.intro, Nat.mem_divisors_self, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
refine_1 : IsRoot (cyclotomic n B) x
⊢ n ≠ 0 ∧ ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x

Tactic:
refine ⟨NeZero.ne n, n, Nat.mem_divisors_self n (NeZero.ne n), ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
refine_1 : Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)
⊢ IsRoot (cyclotomic n B) x

Tactic:
rw [IsRoot.def, ← map_cyclotomic n (algebraMap A B), eval_map_algebraMap]

Premises used: Algebra.algebraMap, Polynomial.IsRoot.def, Polynomial.eval_map_algebraMap, Polynomial.map_cyclotomic
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
⊢ Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)

Tactic:
hx.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
⊢ Eq.{v + 1} (α := B) ((aeval x : (a : A[X]) → B) (cyclotomic n A) : B) (0 : B)

Tactic:
exact hx.2

Premises used: And.right
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
refine_2 : ∀ i < n, ∀ (hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1), ζ ^ i ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)
⊢ x ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)

Tactic:
obtain ⟨i, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx.2

Premises used: And.right, IsPrimitiveRoot.eq_pow_of_pow_eq_one, rfl