awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k n : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ hζ.integralPowerBasisOfPrimePow.gen =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯ + 1

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

Premises used: IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, IsPrimitiveRoot.toInteger, NumberField.RingOfIntegers.ext_iff
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ hζ.subOneIntegralPowerBasisOfPrimePow.gen =
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯

Tactic:
simp [subOneIntegralPowerBasisOfPrimePow]

Premises used: IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Prime (hζ.toInteger - 1)

Tactic:
Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_

Premises used: Ideal.prime_of_irreducible_absNorm_span
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
refine_1 : ∀ (h : hζ.toInteger - 1 = 0), False
refine_2 : Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)
⊢ Prime (hζ.toInteger - 1)

Tactic:
refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_

Premises used: Ideal.prime_of_irreducible_absNorm_span
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h : hζ.toInteger - 1 = 0
⊢ k + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h : hζ.toInteger - 1 = 0
refine_1 : HPow.hPow (β := ℕ) ζ 1 = 1
⊢ False

Tactic:
apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ hp.out.one_lt (by simp))

Premises used: IsPrimitiveRoot.pow_ne_one_of_pos_of_lt, Nat.Prime.one_lt, one_ne_zero, one_lt_pow₀, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h : hζ.toInteger - 1 = 0
⊢ hζ.toInteger = 1

Tactic:
rw [sub_eq_zero] at h

Premises used: sub_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h : hζ.toInteger = 1
⊢ HPow.hPow (β := ℕ) ζ 1 = 1

Tactic:
simpa using congrArg (algebraMap _ K) h

Premises used: Algebra.algebraMap, congrArg, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
refine_2 : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
⊢ Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)

Tactic:
rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
    ← Int.prime_iff_natAbs_prime]

Premises used: Nat.prime_iff, Nat.irreducible_iff_prime, Int.prime_iff_natAbs_prime, Ideal.absNorm_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Prime (M := ℤ) (↑p : ℤ)

Tactic:
Nat.prime_iff_prime_int.1 hp.out

Premises used: Nat.prime_iff_prime_int, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
convert! Nat.prime_iff_prime_int.1 hp.out

Premises used: Nat.prime_iff_prime_int, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h :
  Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
apply RingHom.injective_int (algebraMap ℤ ℚ)

Premises used: Algebra.algebraMap, Rat, Int, RingHom.injective_int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
h :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ)
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ)

Tactic:
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]

Premises used: Algebra.norm_localization, nonZeroDivisors, Int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((↑p : ℚ) : ℚ)

Tactic:
hζ.norm_sub_one_of_prime_ne_two (Polynomial.cyclotomic.irreducible_rat (NeZero.pos _)) hodd

Premises used: IsPrimitiveRoot.norm_sub_one_of_prime_ne_two, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((↑p : ℚ) : ℚ)

Tactic:
exact hζ.norm_sub_one_of_prime_ne_two (Polynomial.cyclotomic.irreducible_rat (NeZero.pos _)) hodd

Premises used: IsPrimitiveRoot.norm_sub_one_of_prime_ne_two, Polynomial.cyclotomic.irreducible_rat, NeZero.pos
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
⊢ NumberField K

Tactic:
have := IsCyclotomicExtension.numberField {2 ^ (k + 1)} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
⊢ Prime (hζ.toInteger - 1)

Tactic:
Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_

Premises used: Ideal.prime_of_irreducible_absNorm_span
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
refine_1 : ∀ (h : hζ.toInteger - 1 = 0), False
refine_2 : Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)
⊢ Prime (hζ.toInteger - 1)

Tactic:
refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_

Premises used: Ideal.prime_of_irreducible_absNorm_span
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
h : hζ.toInteger - 1 = 0
⊢ LT.lt (α := ℕ) 1 2

Tactic:
decide
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
h : hζ.toInteger - 1 = 0
⊢ k + 1 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
h : hζ.toInteger - 1 = 0
refine_1 : HPow.hPow (β := ℕ) ζ 1 = 1
⊢ False

Tactic:
apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ (by decide) (by simp))

Premises used: IsPrimitiveRoot.pow_ne_one_of_pos_of_lt, one_ne_zero, one_lt_pow₀
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
h : hζ.toInteger - 1 = 0
⊢ hζ.toInteger = 1

Tactic:
rw [sub_eq_zero] at h

Premises used: sub_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ HPow.hPow (β := ℕ) ζ 1 = 1

Tactic:
simpa using congrArg (algebraMap _ K) h

Premises used: Algebra.algebraMap, congrArg, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
refine_2 : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
⊢ Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)

Tactic:
rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
    ← Int.prime_iff_natAbs_prime]

Premises used: Nat.prime_iff, Nat.irreducible_iff_prime, Int.prime_iff_natAbs_prime, Ideal.absNorm_span_singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
this : NumberField K
refine_2 :
  ∀ [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))),
    Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
refine_2₁ :
  ∀ (n : ℕ) [IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K]
    (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))),
    Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
cases k
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
⊢ Prime (M := ℤ) (-2)

Tactic:
Prime.neg Int.prime_two

Premises used: Prime.neg, Int.prime_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
h : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (-2 : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
convert! Prime.neg Int.prime_two

Premises used: Prime.neg, Int.prime_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
h :
  Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (-2) : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (-2 : ℤ)

Tactic:
apply RingHom.injective_int (algebraMap ℤ ℚ)

Premises used: Algebra.algebraMap, Rat, Int, RingHom.injective_int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
h :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (-2) : ℚ)
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (-2) : ℚ)

Tactic:
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]

Premises used: Algebra.norm_localization, nonZeroDivisors, Int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
⊢ 0 < HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp only [zero_add, pow_one, Nat.ofNat_pos]

Premises used: Nat.ofNat_pos, zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    (-2 : ℚ)

Tactic:
simpa only [zero_add, pow_one, AddSubgroupClass.coe_sub, OneMemClass.coe_one,
        pow_zero]
      using hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat
        (by simp only [zero_add, pow_one, Nat.ofNat_pos]))

Premises used: AddSubgroupClass.coe_sub, OneMemClass.coe_one, zero_add, pow_zero, IsPrimitiveRoot.norm_pow_sub_one_two, pow_one, Polynomial.cyclotomic.irreducible_rat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
n : ℕ
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))
⊢ Prime (M := ℤ) 2

Tactic:
Int.prime_two

Premises used: Int.prime_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
n : ℕ
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))
h : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
convert! Int.prime_two

Premises used: Int.prime_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
n : ℕ
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))
h :
  Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)

Tactic:
apply RingHom.injective_int (algebraMap ℤ ℚ)

Premises used: Algebra.algebraMap, Rat, Int, RingHom.injective_int
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
n : ℕ
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))
h :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 2 : ℚ)
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)

Tactic:
rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), algebraMap_int_eq]

Premises used: Algebra.norm_localization, nonZeroDivisors, Int, algebraMap_int_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
n : ℕ
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))
⊢ 0 < HPow.hPow (α := ℕ) 2 (n + 1 + 1)

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
this : NumberField K
n : ℕ
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (n + 1 + 1))
⊢ Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 2 : ℚ)

Tactic:
exact hζ.norm_sub_one_two Nat.AtLeastTwo.prop (cyclotomic.irreducible_rat (by simp))

Premises used: Nat.AtLeastTwo.prop, Polynomial.cyclotomic.irreducible_rat, IsPrimitiveRoot.norm_sub_one_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
pos : ∀ (htwo : p = 2), Prime (hζ.toInteger - 1)
neg : ∀ (htwo : ¬p = 2), Prime (hζ.toInteger - 1)
⊢ Prime (hζ.toInteger - 1)

Tactic:
by_cases htwo : p = 2
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p = 2
⊢ Fact (Nat.Prime 2)

Tactic:
subst htwo
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p = 2
hp₁ : Fact (Nat.Prime 2)
⊢ IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K

Tactic:
subst htwo
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst_1 : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_2 : CharZero K
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p = 2
hp₁ : Fact (Nat.Prime 2)
inst : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))

Tactic:
subst htwo
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
hp : Fact (Nat.Prime 2)
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
⊢ Prime (hζ.toInteger - 1)

Tactic:
apply hζ.zeta_sub_one_prime_of_two_pow

Premises used: IsPrimitiveRoot.zeta_sub_one_prime_of_two_pow
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p = 2
⊢ Prime (hζ.toInteger - 1)

Tactic:
apply hζ.zeta_sub_one_prime_of_ne_two htwo

Premises used: IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simpa only [zero_add, pow_one]

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
convert! : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
⊢ Prime (hζ.toInteger - 1)

Tactic:
convert! zeta_sub_one_prime (k := 0) (by simpa only [zero_add, pow_one])

Premises used: IsPrimitiveRoot.zeta_sub_one_prime
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
h : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K

Tactic:
simpa only [zero_add, pow_one]

Premises used: zero_add, pow_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Prime hζ.subOneIntegralPowerBasisOfPrimePow.gen

Tactic:
simpa only [subOneIntegralPowerBasisOfPrimePow_gen] using hζ.zeta_sub_one_prime

Premises used: IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, IsPrimitiveRoot.zeta_sub_one_prime
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
n : ℕ
inst_2 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
n : ℕ
inst_2 : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
h₁ : 2 < n
h₂ : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℕ), p ^ k ≠ n
this : NumberField K
⊢ NeZero n

Tactic:
have : NeZero n := NeZero.of_gt h₁