awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ ∀ (ha' : n ≠ 0), ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n

Tactic:
exact fun _ ↦ ⟨ζ, hζ⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
refine_2 :
  Eq (α := Subalgebra K (CyclotomicField n K)) (adjoin K (rootSet (cyclotomic n K) (SplittingField (cyclotomic n K))))
    (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
⊢ ∀ (x : CyclotomicField n K),
    Membership.mem (γ := Subalgebra K (CyclotomicField n K))
      (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}) x

Tactic:
rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm]

Premises used: eq_comm, Algebra.eq_top_iff, Polynomial.SplittingField.adjoin_rootSet
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra K (CyclotomicField n K)) (adjoin K (rootSet (cyclotomic n K) (SplittingField (cyclotomic n K))))
    (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

Premises used: setOf, CyclotomicField, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra K (CyclotomicField n K)) (adjoin K (rootSet (cyclotomic n K) (SplittingField (cyclotomic n K))))
    (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})

Tactic:
exact IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
⊢ ∀ {n : ℕ} (ha : Membership.mem (γ := Set ℕ) {0} n) (ha' : n ≠ 0), ∃ (r : CyclotomicField 0 K), IsPrimitiveRoot r n

Tactic:
aesop
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
x : CyclotomicField 0 K
⊢ IsSplittingField K K (cyclotomic 0 K)

Tactic:
have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) :=
        Polynomial.isSplittingField_C 1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
x : CyclotomicField 0 K
this : IsSplittingField K K (cyclotomic 0 K)
e : K ≃ₗ[K] CyclotomicField 0 K :=
  (↑(IsSplittingField.algEquiv K (cyclotomic 0 K)) : K ≃ₗ[K] (cyclotomic 0 K).SplittingField)
⊢ finrank K (CyclotomicField 0 K) = 1

Tactic:
simp [← LinearEquiv.finrank_eq e, finrank_self]

Premises used: LinearEquiv.finrank_eq, Module.finrank_self
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
x : CyclotomicField 0 K
⊢ finrank K (CyclotomicField 0 K) = 1

Tactic:
have finrank : Module.finrank K (CyclotomicField 0 K) = 1 := by
      have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) :=
        Polynomial.isSplittingField_C 1
      let e : K ≃ₗ[K] (CyclotomicField 0 K) :=
        (Polynomial.IsSplittingField.algEquiv K (Polynomial.cyclotomic 0 K)).toLinearEquiv
      simp [← LinearEquiv.finrank_eq e, finrank_self]
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
x : CyclotomicField 0 K
finrank : Module.finrank K (CyclotomicField 0 K) = 1
⊢ Membership.mem (γ := Subalgebra K (CyclotomicField 0 K))
    (adjoin K {b : CyclotomicField 0 K | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {0} n ∧ n ≠ 0 ∧ b ^ n = 1}) x

Tactic:
simp [Subalgebra.bot_eq_top_iff_finrank_eq_one.mpr finrank]

Premises used: Iff.mpr, Subalgebra.bot_eq_top_iff_finrank_eq_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : CharZero K
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)

Tactic:
match n with
  | 0 => inferInstance
  | _ + 1 => inferInstance

Premises used: inferInstance, IsCyclotomicExtension, CyclotomicField, Singleton.singleton, _private.0.CyclotomicField.instIsCyclotomicExtensionSingletonNatSetOfCharZero.match_1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : NumberField K
⊢ NumberField.{w} (CyclotomicField n K)

Tactic:
IsCyclotomicExtension.numberField {n} K _

Premises used: IsCyclotomicExtension.numberField, Singleton.singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsDomain A
inst_9 : IsFractionRing A K
rw :
  Function.Injective.{u + 1, w + 1} (α := A) (β := CyclotomicField n K)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (CyclotomicField n K)) (algebraMap A K)) :
      (a : A) → CyclotomicField n K)
⊢ IsTorsionFree.{u, w} A (CyclotomicField n K)

Tactic:
rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective,
    IsScalarTower.algebraMap_eq A K (CyclotomicField n K)]

Premises used: faithfulSMul_iff_algebraMap_injective, Module.isTorsionFree_iff_faithfulSMul, CyclotomicField, IsScalarTower.algebraMap_eq
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsDomain A
inst_9 : IsFractionRing A K
⊢ Function.Injective.{u + 1, w + 1} (α := A) (β := CyclotomicField n K)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (CyclotomicField n K)) (algebraMap A K)) :
      (a : A) → CyclotomicField n K)

Tactic:
(Function.Injective.comp (FaithfulSMul.algebraMap_injective K (CyclotomicField n K))
      (IsFractionRing.injective A K) :)

Premises used: IsFractionRing.injective, Submodule.Quotient.mk, Function.Injective.comp, FaithfulSMul.algebraMap_injective, CyclotomicField
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsDomain A
inst_9 : IsFractionRing A K
⊢ Function.Injective.{u + 1, w + 1} (α := A) (β := CyclotomicField n K)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (CyclotomicField n K)) (algebraMap A K)) :
      (a : A) → CyclotomicField n K)

Tactic:
exact
    (Function.Injective.comp (FaithfulSMul.algebraMap_injective K (CyclotomicField n K))
      (IsFractionRing.injective A K) :)

Premises used: IsFractionRing.injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective, CyclotomicField
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n_1 : ℕ
inst : NeZero n_1
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
n : ℕ
⊢ Eq (α := Algebra ℤ (CyclotomicRing n ℤ ℚ)) (algebraBase n ℤ ℚ) (Ring.toIntAlgebra (CyclotomicRing n ℤ ℚ))

Tactic:
rfl

Premises used: Set.Mem, Submodule.Quotient.mk, QuotientAddGroup.Quotient.addGroup._aux_9, RingCon.toQuotient, Finsupp.onFinset, AddMonoidAlgebra.addAddCommGroup._aux_6, Quot.map, RingHom.codRestrict, Quotient.map', Finsupp.mapRange, CyclotomicRing, rfl, Finsupp.single
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsDomain A
inst_9 : IsFractionRing A K
⊢ IsTorsionFree.{u, w} A (CyclotomicRing n A K)

Tactic:
(adjoin A _).instIsTorsionFree

Premises used: Set.Mem, Subalgebra.instIsTorsionFree, Algebra.adjoin, CyclotomicRing
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
A : Type u
K : Type w
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
inst_3 : IsDomain A
inst_4 : IsFractionRing A K
⊢ Function.Injective.{u + 1, w + 1} (α := A) (β := CyclotomicRing n A K)
    (⇑(algebraMap A (CyclotomicRing n A K)) : (a : A) → CyclotomicRing n A K)

Tactic:
FaithfulSMul.algebraMap_injective _ _

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
A : Type u
K : Type w
inst : CommRing A
inst_1 : Field K
inst_2 : Algebra A K
⊢ Function.Injective.{w + 1, w + 1} (α := CyclotomicRing n A K) (β := CyclotomicField n K)
    (⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) : (a : CyclotomicRing n A K) → CyclotomicField n K)

Tactic:
Subtype.val_injective

Premises used: Subtype.val_injective, CyclotomicRing
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
⊢ IsTorsionFree.{w, w} (CyclotomicRing n A K) (CyclotomicField n K)

Tactic:
isTorsionFree_iff_algebraMap_injective.mpr (adjoin_algebra_injective n A K)

Premises used: Iff.mpr, Module.isTorsionFree_iff_algebraMap_injective, CyclotomicRing.adjoin_algebra_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
⊢ IsScalarTower.{u, w, w} A (CyclotomicRing n A K) (CyclotomicField n K)

Tactic:
inferInstanceAs <| IsScalarTower A (adjoin A _) (CyclotomicField n K)

Premises used: _private.0.CyclotomicRing.instIsScalarTowerCyclotomicField._proof_1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
rw :
  Ne (α := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
              Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
          CyclotomicRing n A K) :
      CyclotomicField n K)
    (0 : CyclotomicField n K)
⊢ IsUnit (M := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
              Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
          CyclotomicRing n A K) :
      CyclotomicField n K)

Tactic:
rw [isUnit_iff_ne_zero]

Premises used: isUnit_iff_ne_zero
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
hg :
  Function.Injective.{w + 1, w + 1} (α := CyclotomicRing n A K) (β := CyclotomicField n K)
    (⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) : (a : CyclotomicRing n A K) → CyclotomicField n K)
h :
  Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K))
    (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
          Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
      CyclotomicRing n A K)
⊢ Ne (α := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
              Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
          CyclotomicRing n A K) :
      CyclotomicField n K)
    (0 : CyclotomicField n K)

Tactic:
apply map_ne_zero_of_mem_nonZeroDivisors

Premises used: map_ne_zero_of_mem_nonZeroDivisors
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
⊢ Function.Injective.{w + 1, w + 1} (α := CyclotomicRing n A K) (β := CyclotomicField n K)
    (⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) : (a : CyclotomicRing n A K) → CyclotomicField n K)

Tactic:
apply adjoin_algebra_injective

Premises used: CyclotomicRing.adjoin_algebra_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
⊢ Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K))
    (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
          Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
      CyclotomicRing n A K)

Tactic:
hx

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
⊢ Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K))
    (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
          Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
      CyclotomicRing n A K)

Tactic:
exact hx
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
⊢ NeZero.{w} (R := K) (↑n : K)

Tactic:
have : NeZero (n : K) := NeZero.nat_of_injective (IsFractionRing.injective A K)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
⊢ ∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) x
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑x_1.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x_1.1

Tactic:
Algebra.adjoin_induction
        (hx := ((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1
            (CyclotomicField.isCyclotomicExtension n K)).2 x)
        (fun y hy => ?_) (fun k => ?_) ?_ ?_

Premises used: Algebra.adjoin_induction, IsCyclotomicExtension.iff_singleton, And.right, CyclotomicField, Iff.mp, CyclotomicField.isCyclotomicExtension
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
y : CyclotomicField n K
hy : Membership.mem (γ := Set (CyclotomicField n K)) {b : CyclotomicField n K | b ^ n = 1} y
simp :
  y =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (Subtype.mk (p := fun (x : CyclotomicField n K) ↦
        Membership.mem (γ := Subalgebra A (CyclotomicField n K)) (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x) y
        ⋯)
⊢ y *
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicField n K) ↦
                  Membership.mem (γ := Subalgebra A (CyclotomicField n K))
                    (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x)
                  y ⋯,
                1).2 :
          CyclotomicRing n A K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (Subtype.mk (p := fun (x : CyclotomicField n K) ↦
            Membership.mem (γ := Subalgebra A (CyclotomicField n K)) (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x)
            y ⋯,
          1).1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
y : CyclotomicField n K
hy : Membership.mem (γ := Set (CyclotomicField n K)) {b : CyclotomicField n K | b ^ n = 1} y
⊢ y =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (Subtype.mk (p := fun (x : CyclotomicField n K) ↦
        Membership.mem (γ := Subalgebra A (CyclotomicField n K)) (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x) y
        ⋯)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
y : CyclotomicField n K
hy : Membership.mem (γ := Set (CyclotomicField n K)) {b : CyclotomicField n K | b ^ n = 1} y
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) y
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑x.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x.1

Tactic:
exact ⟨⟨⟨y, subset_adjoin hy⟩, 1⟩, by simp; rfl⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
k : K
⊢ IsLocalization.{u, w} (R := A) (nonZeroDivisors A) K

Tactic:
have : IsLocalization (nonZeroDivisors A) K := inferInstance