awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ ζ ^ i ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)

Tactic:
SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)

Premises used: Iff.mpr, Algebra.subset_adjoin, SetLike.mem_coe, Subalgebra.pow_mem
-- 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
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
refine_2 : ζ ∈ rootSet (cyclotomic n A) B
⊢ ζ ^ i ∈ (↑(adjoin A (rootSet (cyclotomic n A) B)) : Set B)

Tactic:
refine SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin ?_) _)

Premises used: Iff.mpr, Algebra.subset_adjoin, SetLike.mem_coe, Subalgebra.pow_mem
-- 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
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
refine_2 : Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) ζ
⊢ ζ ∈ rootSet (cyclotomic n A) B

Tactic:
rw [mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, map_cyclotomic, ← IsRoot]

Premises used: Polynomial.IsRoot, Polynomial.mem_rootSet', 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
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) ζ

Tactic:
⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos n)⟩

Premises used: Polynomial.cyclotomic_ne_zero, And.intro, NeZero.pos, IsPrimitiveRoot.isRoot_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
i : ℕ
left : i < n
hx : n ≠ 0 ∧ (ζ ^ i) ^ n = 1
⊢ Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) ζ

Tactic:
exact ⟨cyclotomic_ne_zero n B, hζ.isRoot_cyclotomic (NeZero.pos 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
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[ζ]

Tactic:
le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono 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
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)
refine_2 : ∀ (x : B) (hx : Membership.mem (γ := Set B) {ζ} x), x ∈ rootSet (cyclotomic n A) B
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) A[ζ]

Tactic:
refine le_antisymm (adjoin_le fun x hx => ?_) (adjoin_mono 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
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
obtain : ∀ i < n, ∀ (hx : ζ ^ i ∈ rootSet (cyclotomic n A) B) (hx : (ζ ^ i) ^ n = 1), ζ ^ i ∈ (↑A[ζ] : Set B)
⊢ x ∈ (↑A[ζ] : Set B)

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

Premises used: IsPrimitiveRoot.eq_pow_of_pow_eq_one, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
i : ℕ
left : i < n
hx_1 : ζ ^ i ∈ rootSet (cyclotomic n A) B
hx : (ζ ^ i) ^ n = 1
⊢ ζ ^ i ∈ (↑A[ζ] : Set B)

Tactic:
SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)

Premises used: Iff.mpr, Set.mem_singleton, Algebra.subset_adjoin, SetLike.mem_coe, Subalgebra.pow_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
i : ℕ
left : i < n
hx_1 : ζ ^ i ∈ rootSet (cyclotomic n A) B
hx : (ζ ^ i) ^ n = 1
⊢ ζ ^ i ∈ (↑A[ζ] : Set B)

Tactic:
exact SetLike.mem_coe.2 (Subalgebra.pow_mem _ (subset_adjoin <| mem_singleton ζ) _)

Premises used: Iff.mpr, Set.mem_singleton, Algebra.subset_adjoin, SetLike.mem_coe, Subalgebra.pow_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
refine_1 : x ^ n = 1
⊢ x ∈ (↑A[ζ] : Set B)

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 ζ) _)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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

Tactic:
(isRoot_of_unity_iff (NeZero.pos n) B).2 ?_

Premises used: Iff.mpr, 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
refine_1 : ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x
⊢ x ^ n = 1

Tactic:
refine (isRoot_of_unity_iff (NeZero.pos n) B).2 ?_

Premises used: Iff.mpr, 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
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

Tactic:
⟨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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
refine_1 : IsRoot (cyclotomic n B) x
⊢ ∃ i ∈ n.divisors, IsRoot (cyclotomic i B) x

Tactic:
refine ⟨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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x ∈ rootSet (cyclotomic n A) B
⊢ Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) x

Tactic:
rw [mem_rootSet', ← eval_map_algebraMap, map_cyclotomic, ← IsRoot] at hx

Premises used: Polynomial.IsRoot, Polynomial.mem_rootSet', 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) x
⊢ IsRoot (cyclotomic n B) x

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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : Ne (α := B[X]) (cyclotomic n B) 0 ∧ IsRoot (cyclotomic n B) x
⊢ IsRoot (cyclotomic n B) x

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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : Membership.mem (γ := Set B) {ζ} x
⊢ x = ζ

Tactic:
simp only [mem_singleton_iff] at hx

Premises used: 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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
hx : x = ζ
⊢ x ∈ rootSet (cyclotomic n A) B

Tactic:
simpa only [hx, mem_rootSet', map_cyclotomic, ← eval_map_algebraMap, IsRoot] using
      And.intro (cyclotomic_ne_zero n B) (hζ.isRoot_cyclotomic (NeZero.pos n))

Premises used: Polynomial.cyclotomic_ne_zero, Polynomial.IsRoot, And.intro, Polynomial.mem_rootSet', NeZero.pos, Polynomial.eval_map_algebraMap, Polynomial.map_cyclotomic, IsPrimitiveRoot.isRoot_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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
rw : Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) ⊤
⊢ Eq (α := Subalgebra A B) A[ζ] ⊤

Tactic:
rw [← adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic hζ]

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_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
n : ℕ
inst_3 : NeZero n
inst_4 : IsDomain B
h : IsCyclotomicExtension {n} A B
ζ : B
hζ : IsPrimitiveRoot ζ n
rw :
  Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
    ⊤
⊢ Eq (α := Subalgebra A B) (adjoin A (rootSet (cyclotomic n A) B)) ⊤

Tactic:
rw [adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ]

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
    ⊤

Tactic:
((iff_adjoin_eq_top {n} A B).mp h).2

Premises used: And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Singleton.singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
    ⊤

Tactic:
exact ((iff_adjoin_eq_top {n} A B).mp h).2

Premises used: And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Singleton.singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)) ⊤
rw₃ :
  Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
    ⊤
⊢ Eq (α := Subalgebra A B) A[ζ] ⊤

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

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Singleton.singleton, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
n_1 : ℕ
hi : Membership.mem (γ := Set ℕ) {n} n_1
hi' : n_1 ≠ 0
⊢ n_1 = n

Tactic:
rw [Set.mem_singleton_iff] at hi

Premises used: 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
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
n_1 : ℕ
hi : Membership.mem (γ := Set ℕ) {n} n_1
hi' : n_1 ≠ 0
hi₁ : n_1 = n
⊢ n_1 ≠ 0

Tactic:
rw [Set.mem_singleton_iff] at hi

Premises used: 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
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
n_1 : ℕ
hi : n_1 = n
hi' : n_1 ≠ 0
⊢ ∃ (r : ↥A[ζ]), IsPrimitiveRoot r n_1

Tactic:
⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩

Premises used: Set.mem_singleton, Algebra.subset_adjoin, Subtype.mk, Exists.intro
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
n_1 : ℕ
hi : n_1 = n
hi' : n_1 ≠ 0
refine :
  IsPrimitiveRoot (M := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n_1
⊢ ∃ (r : ↥A[ζ]), IsPrimitiveRoot r n_1

Tactic:
refine ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
n_1 : ℕ
hi : n_1 = n
hi' : n_1 ≠ 0
rwa : IsPrimitiveRoot (↑(Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) : B) n_1
rwa₁ : IsPrimitiveRoot ζ n_1
rwa₂ rwa₃ rwa₄ rwa₅ : IsPrimitiveRoot ζ n
⊢ IsPrimitiveRoot (M := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n_1

Tactic:
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]

Premises used: Subtype.coe_mk, IsPrimitiveRoot.coe_submonoidClass_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
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) x hx)

Tactic:
adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)

Premises used: Algebra.adjoin_induction
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
refine_1 :
  ∀ (b : B) (hb : Membership.mem (γ := Set B) {ζ} b),
    Membership.mem (γ := Subalgebra A ↥A[ζ])
      (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b ⋯)
refine_2 :
  ∀ (a : A),
    Membership.mem.{v, v} (α := ↥A[ζ]) (γ := Subalgebra A ↥A[ζ])
      (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ((algebraMap A B : (a : A) → B) a)
          ⋯ :
        ↥A[ζ])
refine_3 :
  ∀ (b₁ b₂ : B) (x : Membership.mem (γ := Subalgebra A B) A[ζ] b₁) (x_2 : Membership.mem (γ := Subalgebra A B) A[ζ] b₂)
    (hb₁ :
      Membership.mem (γ := Subalgebra A ↥A[ζ])
        (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₁ x))
    (hb₂ :
      Membership.mem (γ := Subalgebra A ↥A[ζ])
        (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₂ x_2)),
    Membership.mem (γ := Subalgebra A ↥A[ζ])
      (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) (b₁ + b₂) ⋯)
refine_4 :
  ∀ (b₁ b₂ : B) (x : Membership.mem (γ := Subalgebra A B) A[ζ] b₁) (x_2 : Membership.mem (γ := Subalgebra A B) A[ζ] b₂)
    (hb₁ :
      Membership.mem (γ := Subalgebra A ↥A[ζ])
        (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₁ x))
    (hb₂ :
      Membership.mem (γ := Subalgebra A ↥A[ζ])
        (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
        (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b₂ x_2)),
    Membership.mem (γ := Subalgebra A ↥A[ζ])
      (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
      (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) (b₁ * b₂) ⋯)
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) x hx)

Tactic:
refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb : Membership.mem (γ := Set B) {ζ} b
⊢ b = ζ

Tactic:
rw [Set.mem_singleton_iff] at hb

Premises used: 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
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b ⋯)

Tactic:
subset_adjoin ?_

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
refine_1 :
  Membership.mem (γ := Set ↥A[ζ]) {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b ⋯)
⊢ Membership.mem (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b ⋯)

Tactic:
refine subset_adjoin ?_

Premises used: Algebra.subset_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
refine_1 :
  n ≠ 0 ∧ HPow.hPow (α := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n = 1
⊢ Membership.mem (γ := Set ↥A[ζ]) {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) b ⋯)

Tactic:
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq, hb]

Premises used: exists_eq_left, Set.mem_setOf_eq, 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
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
refine_1 : n ≠ 0 ∧ ζ ^ n = 1
⊢ n ≠ 0 ∧ HPow.hPow (α := ↥A[ζ]) (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ζ ⋯) n = 1

Tactic:
rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]

Premises used: Subtype.coe_mk, Subalgebra.coe_eq_one, Subalgebra.coe_pow
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
⊢ n ≠ 0 ∧ ζ ^ n = 1

Tactic:
⟨NeZero.ne n, ((IsPrimitiveRoot.iff_def ζ n).1 h).1⟩

Premises used: IsPrimitiveRoot.iff_def, And.left, And.intro, Iff.mp, 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
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
b : B
hb_1 : Membership.mem (γ := Set B) {ζ} b
hb : b = ζ
⊢ n ≠ 0 ∧ ζ ^ n = 1

Tactic:
exact ⟨NeZero.ne n, ((IsPrimitiveRoot.iff_def ζ n).1 h).1⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
a : A
⊢ Membership.mem.{v, v} (α := ↥A[ζ]) (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ((algebraMap A B : (a : A) → B) a) ⋯ :
      ↥A[ζ])

Tactic:
Subalgebra.algebraMap_mem _ _

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
ζ : B
n : ℕ
inst_3 : NeZero n
h : IsPrimitiveRoot ζ n
x_1 : ↥A[ζ]
x : B
hx : Membership.mem (γ := Subalgebra A B) A[ζ] x
a : A
⊢ Membership.mem.{v, v} (α := ↥A[ζ]) (γ := Subalgebra A ↥A[ζ])
    (adjoin A {b : ↥A[ζ] | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
    (Subtype.mk (p := fun (x : B) ↦ Membership.mem (γ := Subalgebra A B) A[ζ] x) ((algebraMap A B : (a : A) → B) a) ⋯ :
      ↥A[ζ])

Tactic:
exact Subalgebra.algebraMap_mem _ _

Premises used: Subalgebra.algebraMap_mem