awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
this_6 : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤

Tactic:
isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _

Premises used: HMul.hMul, Rat, IntermediateField.isCyclotomicExtension_eq, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
this_6 : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤

Tactic:
exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _

Premises used: HMul.hMul, Rat, IntermediateField.isCyclotomicExtension_eq, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤

Tactic:
have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ

Premises used: _private.0.IsCyclotomicExtension.Rat.adjoin_singleton_eq_top_aux, Rat, HPow.hPow, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
exact adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ

Premises used: _private.0.IsCyclotomicExtension.Rat.adjoin_singleton_eq_top_aux, Rat, HPow.hPow, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
algebraMap_injective : Function.Injective (α := ↥ℤ[ζ]) (β := K) (⇑(algebraMap (↥ℤ[ζ]) K) : (a : ↥ℤ[ζ]) → K)
isIntegral_iff : ∀ {x : K}, IsIntegral ℤ x ↔ ∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K

Tactic:
constructor
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ Function.Injective (α := ↥ℤ[ζ]) (β := K) (⇑(algebraMap (↥ℤ[ζ]) K) : (a : ↥ℤ[ζ]) → K)

Tactic:
FaithfulSMul.algebraMap_injective _ K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ Function.Injective (α := ↥ℤ[ζ]) (β := K) (⇑(algebraMap (↥ℤ[ζ]) K) : (a : ↥ℤ[ζ]) → K)

Tactic:
exact FaithfulSMul.algebraMap_injective _ K

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x : K
⊢ Eq (α := Subalgebra ℤ K) (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ℤ[hζ.toInteger])
    (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ⊤)

Tactic:
have := congr_arg (Subalgebra.map (IsScalarTower.toAlgHom ℤ (𝓞 K) K))
      (adjoin_singleton_eq_top hζ)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x : K
this :
  Eq (α := Subalgebra ℤ K) (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ℤ[hζ.toInteger])
    (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ⊤)
⊢ Eq (α := Subalgebra ℤ K) ℤ[ζ] (AlgHom.range (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K))

Tactic:
simp only [AlgHom.map_adjoin_singleton, IsScalarTower.coe_toAlgHom', RingOfIntegers.map_mk,
      Algebra.map_top] at this

Premises used: IsScalarTower.coe_toAlgHom', Algebra.map_top, AlgHom.map_adjoin_singleton, NumberField.RingOfIntegers.map_mk
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x : K
this : Eq (α := Subalgebra ℤ K) ℤ[ζ] (AlgHom.range (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K))
⊢ IsIntegral ℤ x ↔ ∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x

Tactic:
simp [IsIntegralClosure.isIntegral_iff (A := 𝓞 K), this, ← SetLike.mem_coe]

Premises used: IsIntegralClosure.isIntegral_iff, SetLike.mem_coe
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
⊢ IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n

Tactic:
have hζ := zeta_spec n ℚ (CyclotomicField n ℚ)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)

Tactic:
⟨IsFractionRing.injective _ _, fun {x} => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩

Premises used: IsFractionRing.injective, IsIntegralClosure.mk, Subtype.mk, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
refine_1 :
  ∀ {x : CyclotomicField n ℚ} (h : IsIntegral ℤ x),
    Membership.mem (γ := Subalgebra ℤ (CyclotomicField n ℚ)) (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1}) x
refine_2 :
  ∀ {x : CyclotomicField n ℚ},
    (∃ (y : CyclotomicRing n ℤ ℚ),
        (algebraMap (CyclotomicRing n ℤ ℚ) (CyclotomicField n ℚ) : (a : CyclotomicRing n ℤ ℚ) → CyclotomicField n ℚ) y =
          x) →
      IsIntegral ℤ x
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)

Tactic:
refine ⟨IsFractionRing.injective _ _, fun {x} => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
x : CyclotomicField n ℚ
h : IsIntegral ℤ x
refine_1 :
  ∀ (y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)])
    (h :
      IsIntegral ℤ (A := CyclotomicField n ℚ)
        ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
              (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
            y :
          CyclotomicField n ℚ)),
    Membership.mem (α := CyclotomicField n ℚ) (γ := Subalgebra ℤ (CyclotomicField n ℚ))
      (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1})
      ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
            (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
          y :
        CyclotomicField n ℚ)
⊢ Membership.mem (γ := Subalgebra ℤ (CyclotomicField n ℚ)) (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1}) x

Tactic:
obtain ⟨y, rfl⟩ := (isIntegralClosure_adjoin_singleton hζ).isIntegral_iff.1 h

Premises used: IsIntegralClosure.isIntegral_iff, Iff.mp, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
⊢ Membership.mem (α := CyclotomicField n ℚ) (γ := Subalgebra ℤ (CyclotomicField n ℚ))
    (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1})
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)

Tactic:
adjoin_mono ?_ y.2

Premises used: Algebra.adjoin_mono, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
refine_1 :
  Subset (α := Set (CyclotomicField n ℚ)) {zeta n ℚ (CyclotomicField n ℚ)} {b : CyclotomicField n ℚ | b ^ n = 1}
⊢ Membership.mem (α := CyclotomicField n ℚ) (γ := Subalgebra ℤ (CyclotomicField n ℚ))
    (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1})
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)

Tactic:
refine adjoin_mono ?_ y.2

Premises used: Algebra.adjoin_mono, Subtype.property
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
refine_1 : HPow.hPow (α := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n = 1
⊢ Subset (α := Set (CyclotomicField n ℚ)) {zeta n ℚ (CyclotomicField n ℚ)} {b : CyclotomicField n ℚ | b ^ n = 1}

Tactic:
simp only [Set.singleton_subset_iff, Set.mem_setOf_eq]

Premises used: Set.singleton_subset_iff, Set.mem_setOf_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
⊢ HPow.hPow (α := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n = 1

Tactic:
hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]
h :
  IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) (CyclotomicField n ℚ) :
          (a : ↥ℤ[zeta n ℚ (CyclotomicField n ℚ)]) → CyclotomicField n ℚ)
        y :
      CyclotomicField n ℚ)
⊢ HPow.hPow (α := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n = 1

Tactic:
exact hζ.pow_eq_one

Premises used: IsPrimitiveRoot.pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : CyclotomicRing n ℤ ℚ
⊢ IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (CyclotomicRing n ℤ ℚ) (CyclotomicField n ℚ) : (a : CyclotomicRing n ℤ ℚ) → CyclotomicField n ℚ) y :
      CyclotomicField n ℚ)

Tactic:
IsIntegral.algebraMap ((IsCyclotomicExtension.integral {n} ℤ _).isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
y : CyclotomicRing n ℤ ℚ
⊢ IsIntegral ℤ (A := CyclotomicField n ℚ)
    ((algebraMap (CyclotomicRing n ℤ ℚ) (CyclotomicField n ℚ) : (a : CyclotomicRing n ℤ ℚ) → CyclotomicField n ℚ) y :
      CyclotomicField n ℚ)

Tactic:
exact IsIntegral.algebraMap ((IsCyclotomicExtension.integral {n} ℤ _).isIntegral _)

Premises used: Algebra.IsIntegral.isIntegral, IsIntegral.algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
⊢ IsCyclotomicExtension.{0, u} {n} ℤ (𝓞 K)

Tactic:
let _ := (zeta_spec n ℚ K).adjoin_isCyclotomicExtension ℤ
  IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec n ℚ K).adjoinEquivRingOfIntegers

Premises used: Rat, Algebra.adjoin, Membership.mem, Subtype, Int, IsCyclotomicExtension.equiv, IsCyclotomicExtension.zeta_spec, IsPrimitiveRoot.adjoin_isCyclotomicExtension, Singleton.singleton, IsPrimitiveRoot.adjoinEquivRingOfIntegers, IsCyclotomicExtension.zeta
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : NeZero n
inst_2 : CharZero K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
rw :
  (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((hζ.adjoinEquivRingOfIntegers : (a : ↥ℤ[ζ]) → 𝓞 K)
          (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) :
        𝓞 K) =
    (↑hζ.toInteger : K)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.integralPowerBasis.gen = (↑hζ.toInteger : K)

Tactic:
rw [integralPowerBasis, PowerBasis.map_gen, adjoin.powerBasis'_gen]

Premises used: PowerBasis.map_gen, IsPrimitiveRoot.integralPowerBasis, Algebra.adjoin.powerBasis'_gen
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : NeZero n
inst_2 : CharZero K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
      ((hζ.adjoinEquivRingOfIntegers : (a : ↥ℤ[ζ]) → 𝓞 K)
          (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x) ζ ⋯) :
        𝓞 K) =
    (↑hζ.toInteger : K)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ hζ.integralPowerBasis.dim = φ n

Tactic:
simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ (NeZero.pos _), natDegree_cyclotomic]

Premises used: Polynomial.natDegree_cyclotomic, IsPrimitiveRoot.integralPowerBasis, NeZero.pos, Polynomial.cyclotomic_eq_minpoly
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯] ⊤

Tactic:
hζ.integralPowerBasis.adjoin_eq_top_of_gen_mem_adjoin ?_

Premises used: PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
refine :
  Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    hζ.integralPowerBasis.gen
⊢ Eq (α := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯] ⊤

Tactic:
refine hζ.integralPowerBasis.adjoin_eq_top_of_gen_mem_adjoin ?_

Premises used: PowerBasis.adjoin_eq_top_of_gen_mem_adjoin
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    (Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯ + 1)

Tactic:
Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Premises used: Subalgebra.add_mem, Int, Subalgebra.one_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h :
  hζ.integralPowerBasis.gen =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯ + 1
⊢ Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    hζ.integralPowerBasis.gen

Tactic:
convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)

Premises used: Subalgebra.add_mem, Int, Subalgebra.one_mem, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ hζ.integralPowerBasis.gen =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯ + 1

Tactic:
simp [RingOfIntegers.ext_iff, integralPowerBasis_gen, toInteger]

Premises used: IsPrimitiveRoot.toInteger, NumberField.RingOfIntegers.ext_iff, IsPrimitiveRoot.integralPowerBasis_gen
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : NeZero n
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ hζ.subOneIntegralPowerBasis.gen =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯

Tactic:
simp [subOneIntegralPowerBasis]

Premises used: IsPrimitiveRoot.subOneIntegralPowerBasis
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ : IsPrimitiveRoot ζ n
rw : n ∣ Nat.card.{u} ↥(torsion K)
⊢ n ∣ torsionOrder K

Tactic:
rw [torsionOrder, Fintype.card_eq_nat_card]

Premises used: NumberField.Units.torsionOrder, Fintype.card_eq_nat_card
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ IsPrimitiveRoot (IsUnit.unit (a := hζ.toInteger) ⋯) n

Tactic:
replace hζ := (hζ.toInteger_isPrimitiveRoot).isUnit_unit (NeZero.ne n)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
⊢ orderOf (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (↑⋯.unit : (𝓞 K)ˣ) ⋯) ∣
    Nat.card.{u} ↥(torsion K)

Tactic:
orderOf_dvd_natCard (⟨(hζ.isUnit (NeZero.ne n)).unit, ?_⟩ : torsion K)

Premises used: Units.val, orderOf_dvd_natCard, IsPrimitiveRoot.isUnit, Subtype.mk, IsUnit.unit, NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
h :
  n =
    orderOf (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (↑⋯.unit : (𝓞 K)ˣ) ⋯)
convert! : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) (↑⋯.unit : (𝓞 K)ˣ)
⊢ n ∣ Nat.card.{u} ↥(torsion K)

Tactic:
convert! orderOf_dvd_natCard (⟨(hζ.isUnit (NeZero.ne n)).unit, ?_⟩ : torsion K)

Premises used: Units.val, orderOf_dvd_natCard, IsPrimitiveRoot.isUnit, Subtype.mk, IsUnit.unit, NeZero.ne
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : NeZero n
inst_2 : NumberField K
ζ : K
hζ_1 : IsPrimitiveRoot ζ n
hζ : IsPrimitiveRoot (IsUnit.unit (a := hζ_1.toInteger) ⋯) n
h : n = orderOf (↑⋯.unit : (𝓞 K)ˣ)
⊢ n =
    orderOf (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (↑⋯.unit : (𝓞 K)ˣ) ⋯)

Tactic:
rw [Subgroup.orderOf_mk]

Premises used: Subgroup.orderOf_mk