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
pos : ∀ (hS : ∃ s ∈ S, s ≠ 0), IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
neg : ∀ (hS : ¬∃ s ∈ S, s ≠ 0), IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
by_cases hS : ∃ s ∈ S, s ≠ 0
-- 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
hS : ∃ s ∈ S, s ≠ 0
⊢ ∃ s ∈ S, s ≠ 0 ∧ 1 ∣ s

Tactic:
simpa
-- 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
hS : ∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
exact iff_union_of_dvd _ _ (by simpa)

Premises used: IsCyclotomicExtension.iff_union_of_dvd
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
⊢ S \ {0} = ∅

Tactic:
aesop
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
⊢ Eq (α := Set ℕ) ({1} \ {0}) {1}

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
hS : ¬∃ s ∈ S, s ≠ 0
neg : IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension S A B ↔ IsCyclotomicExtension (S ∪ {1}) A B

Tactic:
rw [eq_self_sdiff_zero S, eq_self_sdiff_zero (S ∪ {1}), union_diff_distrib,
      show S \ {0} = ∅ by aesop, empty_union, show {1} \ {0} = {1} by simp]

Premises used: Set.empty_union, Set.union_diff_distrib, IsCyclotomicExtension.eq_self_sdiff_zero, Union.union, 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
hS : ¬∃ s ∈ S, s ≠ 0
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B

Tactic:
⟨fun H ↦ ?_, fun H ↦ ?_⟩

Premises used: Iff.intro
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
neg : ∀ (H : IsCyclotomicExtension ∅ A B), IsCyclotomicExtension {1} A B
neg₁ : ∀ (H : IsCyclotomicExtension {1} A B), IsCyclotomicExtension ∅ A B
⊢ IsCyclotomicExtension ∅ A B ↔ IsCyclotomicExtension {1} A B

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension ∅ A B
s : ℕ
hs : Membership.mem (γ := Set ℕ) {1} s
h : s ≠ 0
⊢ IsPrimitiveRoot.{v} (M := B) 1 s

Tactic:
simp [mem_singleton_iff.1 hs]

Premises used: Set.mem_singleton_iff, Iff.mp
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension ∅ A B
neg :
  Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {1} n ∧ n ≠ 0 ∧ b ^ n = 1})
    ⊤
⊢ IsCyclotomicExtension {1} A B

Tactic:
refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs _ ↦ ⟨1, by simp [mem_singleton_iff.1 hs]⟩, ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, IsCyclotomicExtension.iff_adjoin_eq_top, 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
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension ∅ A B
⊢ Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {1} n ∧ n ≠ 0 ∧ b ^ n = 1})
    ⊤

Tactic:
simpa [adjoin_singleton_one] using subsingleton_iff_bot_eq_top.mpr inferInstance

Premises used: Iff.mpr, inferInstance, Algebra.adjoin_singleton_one, subsingleton_iff_bot_eq_top
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
⊢ IsCyclotomicExtension ∅ A B

Tactic:
(iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩

Premises used: Iff.mpr, False.elim, And.intro, Set.notMem_empty, IsCyclotomicExtension.iff_adjoin_eq_top
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
neg :
  Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) ∅ n ∧ n ≠ 0 ∧ b ^ n = 1}) ⊤
⊢ IsCyclotomicExtension ∅ A B

Tactic:
refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs ↦ (notMem_empty s hs).elim, ?_⟩

Premises used: Iff.mpr, False.elim, And.intro, Set.notMem_empty, IsCyclotomicExtension.iff_adjoin_eq_top
-- 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
hS : ¬∃ s ∈ S, s ≠ 0
H : IsCyclotomicExtension {1} A B
⊢ Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) ∅ n ∧ n ≠ 0 ∧ b ^ n = 1}) ⊤

Tactic:
simp [singleton_one]

Premises used: IsCyclotomicExtension.singleton_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
h₁ : Eq (α := Set ℕ) {1} (({0} ∪ {1}) \ {0})
⊢ IsCyclotomicExtension {1} A B

Tactic:
convert!
    eq_self_sdiff_zero _ A B ▸ (iff_union_singleton_one _ A _).1 (singleton_zero_of_bot_eq_top h)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
⊢ Eq (α := Set ℕ) {1} (({0} ∪ {1}) \ {0})

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : Function.Surjective.{u + 1, v + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
⊢ IsCyclotomicExtension {1} A B

Tactic:
singleton_one_of_bot_eq_top (surjective_algebraMap_iff.1 h).symm

Premises used: Algebra.surjective_algebraMap_iff, Iff.mp, IsCyclotomicExtension.singleton_one_of_bot_eq_top, Eq.symm
-- 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
C : Type u_1
inst_3 : CommRing C
inst_4 : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this : Algebra B C := (↑f : B →ₐ[A] C).toAlgebra
⊢ IsCyclotomicExtension {1} B C

Tactic:
haveI : IsCyclotomicExtension {1} B C := singleton_one_of_algebraMap_bijective f.surjective
-- 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
C : Type u_1
inst_3 : CommRing C
inst_4 : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this_1 : Algebra B C := (↑f : B →ₐ[A] C).toAlgebra
this : IsCyclotomicExtension {1} B C
⊢ IsScalarTower A B C

Tactic:
haveI : IsScalarTower A B C := IsScalarTower.of_algHom f.toAlgHom
-- 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
C : Type u_1
inst_3 : CommRing C
inst_4 : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this_1 : Algebra B C := (↑f : B →ₐ[A] C).toAlgebra
this_2 : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C

Tactic:
(iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)

Premises used: Iff.mpr, IsCyclotomicExtension.trans, AlgEquiv.injective, Singleton.singleton, OfNat.ofNat, IsCyclotomicExtension.iff_union_singleton_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
C : Type u_1
inst_3 : CommRing C
inst_4 : Algebra A C
h : IsCyclotomicExtension S A B
f : B ≃ₐ[A] C
this_1 : Algebra B C := (↑f : B →ₐ[A] C).toAlgebra
this_2 : IsCyclotomicExtension {1} B C
this : IsScalarTower A B C
⊢ IsCyclotomicExtension S A C

Tactic:
exact (iff_union_singleton_one _ _ _).2 (trans S {1} A B C f.injective)

Premises used: Iff.mpr, IsCyclotomicExtension.trans, AlgEquiv.injective, Singleton.singleton, OfNat.ofNat, IsCyclotomicExtension.iff_union_singleton_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension S A B
inst_5 : IsDomain B
hn : n ∈ S
⊢ NeZero.{v} (R := B) (↑n : B)

Tactic:
(exists_isPrimitiveRoot A B hn NeZero.out).choose_spec.neZero'

Premises used: Exists.choose_spec, IsCyclotomicExtension.exists_isPrimitiveRoot, IsPrimitiveRoot.neZero', NeZero.out
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsCyclotomicExtension S A B
inst_5 : IsDomain B
hn : n ∈ S
⊢ NeZero.{u} (R := A) (↑n : A)

Tactic:
(neZero_of_mem n S A B hn).nat_of_neZero (algebraMap A B)

Premises used: Algebra.algebraMap, NeZero.nat_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 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
⊢ NeZero.{v} (R := B) (↑n : B)

Tactic:
neZero_of_mem n {n} A B (mem_singleton n)

Premises used: IsCyclotomicExtension.neZero_of_mem, Set.mem_singleton, Singleton.singleton
-- 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 : IsCyclotomicExtension {n} A B
inst_5 : IsDomain B
⊢ NeZero.{u} (R := A) (↑n : A)

Tactic:
neZero_of_mem' n {n} A B (mem_singleton n)

Premises used: Set.mem_singleton, IsCyclotomicExtension.neZero_of_mem', Singleton.singleton
-- 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
rw : Algebra.IsIntegral.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
⊢ Algebra.IsIntegral A B

Tactic:
rw [← (Subalgebra.equivOfEq _ _ ((IsCyclotomicExtension.iff_adjoin_eq_top S A B).1 ‹_›).2
    |>.trans Subalgebra.topEquiv).isIntegral_iff]

Premises used: Subalgebra.equivOfEq, AlgEquiv.isIntegral_iff, AlgEquiv.trans, And.right, Iff.mp, IsCyclotomicExtension.iff_adjoin_eq_top, Subalgebra.topEquiv
-- 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
x : B
h : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ eval₂ (algebraMap A B) x (HPow.hPow (α := A[X]) X n - 1) = 0

Tactic:
simp [h2]
-- 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
⊢ Algebra.IsIntegral.{u, v} A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})

Tactic:
exact Algebra.IsIntegral.adjoin fun x ⟨n, hn, h1, h2⟩ ↦
    ⟨X ^ n - 1, monic_X_pow_sub_C 1 h1, by simp [h2]⟩
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
obtain :
  ∀ (r : B) (hr1 : r ^ n = 1) (hr2 : ∀ (l : ℕ), r ^ l = 1 → n ∣ l),
    ∃ (r : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})), IsPrimitiveRoot r n
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})), IsPrimitiveRoot r n

Tactic:
obtain ⟨r, hr1, hr2⟩ := h n hn1 hn2
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
r : B
hr1 : r ^ n = 1
hr2 : ∀ (l : ℕ), r ^ l = 1 → n ∣ l
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})), IsPrimitiveRoot r n

Tactic:
⟨⟨r, subset_adjoin ⟨n, hn1, hn2, hr1⟩⟩, Subtype.val_injective hr1,
      fun l hl ↦ hr2 l congr($hl.1)⟩

Premises used: IsPrimitiveRoot.mk, congrArg, Subtype.val_injective, Algebra.subset_adjoin, id, Subtype.mk, And.intro, Exists.intro, Subtype.val
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
r : B
hr1 : r ^ n = 1
hr2 : ∀ (l : ℕ), r ^ l = 1 → n ∣ l
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})), IsPrimitiveRoot r n

Tactic:
exact ⟨⟨r, subset_adjoin ⟨n, hn1, hn2, hr1⟩⟩, Subtype.val_injective hr1,
      fun l hl ↦ hr2 l congr($hl.1)⟩
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
x_1 x : B
hx : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x
mem :
  ∀ (n : ℕ) (hn1 : n ∈ S) (hn2 : n ≠ 0) (hx : x ^ n = 1),
    Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
      (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
      (Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x ⋯)
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x ⋯)

Tactic:
obtain ⟨n, hn1, hn2, hx⟩ := hx
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
x_1 x : B
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
hx : x ^ n = 1
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x ⋯)

Tactic:
subset_adjoin ⟨n, hn1, hn2, Subtype.val_injective hx⟩

Premises used: Subtype.val_injective, Algebra.subset_adjoin, And.intro, Exists.intro
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
x_1 x : B
n : ℕ
hn1 : n ∈ S
hn2 : n ≠ 0
hx : x ^ n = 1
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x ⋯)

Tactic:
exact subset_adjoin ⟨n, hn1, hn2, Subtype.val_injective hx⟩
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
x_1 : B
x : A
⊢ Membership.mem.{v, v} (α := ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) (γ :=
    Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
        ((algebraMap A B : (a : A) → B) x) ⋯ :
      ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))

Tactic:
Subalgebra.algebraMap_mem _ x

Premises used: Set.Mem, Subalgebra.algebraMap_mem
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
x_1 : B
x : A
⊢ Membership.mem.{v, v} (α := ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) (γ :=
    Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
        ((algebraMap A B : (a : A) → B) x) ⋯ :
      ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))

Tactic:
exact Subalgebra.algebraMap_mem _ x

Premises used: Subalgebra.algebraMap_mem
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
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 :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx)
ihy :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) y hy)
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) (x + y) ⋯)

Tactic:
Subalgebra.add_mem _ ihx ihy

Premises used: Set.Mem, Subalgebra.add_mem
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
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 :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx)
ihy :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) y hy)
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) (x + y) ⋯)

Tactic:
exact Subalgebra.add_mem _ ihx ihy

Premises used: Subalgebra.add_mem
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
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 :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx)
ihy :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) y hy)
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) (x * y) ⋯)

Tactic:
Subalgebra.mul_mem _ ihx ihy

Premises used: Subalgebra.mul_mem, Set.Mem
-- 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
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
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 :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx)
ihy :
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) y hy)
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) (x * y) ⋯)

Tactic:
exact Subalgebra.mul_mem _ ihx ihy

Premises used: Subalgebra.mul_mem
-- 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)
h : ∀ (x : B), Eq (α := B) ((f : (a : B) → B) x : B) ((g : (a : B) → B) x : B)
⊢ f = g

Tactic:
ext x
-- 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
⊢ Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x

Tactic:
have hx := ‹IsCyclotomicExtension S A B›.adjoin_roots x