awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : NumberField K
h : hζ.toInteger = 1
⊢ False

Tactic:
exact hζ.ne_one (one_lt_pow₀ hp.1.one_lt (Nat.zero_ne_add_one k).symm)
    (RingOfIntegers.ext_iff.1 h)

Premises used: Nat.Prime.one_lt, Ne.symm, Iff.mp, NumberField.RingOfIntegers.ext_iff, one_lt_pow₀, IsPrimitiveRoot.ne_one, Fact.out, Nat.zero_ne_add_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
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K

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

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

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

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ_1 : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ_1.toInteger - 1}))

Tactic:
hζ.finite_quotient_span_sub_one

Premises used: IsPrimitiveRoot.finite_quotient_span_sub_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
hcycl : IsCyclotomicExtension {p} ℚ K
hζ_1 : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Finite.{u + 1} (HasQuotient.Quotient (𝓞 K) (B := Ideal (𝓞 K)) (Ideal.span {hζ_1.toInteger - 1}))

Tactic:
exact hζ.finite_quotient_span_sub_one

Premises used: IsPrimitiveRoot.finite_quotient_span_sub_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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
pos : ∀ (htwo : p ^ (k + 1) = 2), hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
neg : ∀ (htwo : ¬p ^ (k + 1) = 2), hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)

Tactic:
by_cases htwo : p ^ (k + 1) = 2

Premises used: HAdd.hAdd, OfNat.ofNat
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
⊢ p = 2

Tactic:
have ⟨hp2, hk⟩ := (Nat.Prime.pow_eq_iff Nat.prime_two).1 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
⊢ k + 1 = 1

Tactic:
have ⟨hp2, hk⟩ := (Nat.Prime.pow_eq_iff Nat.prime_two).1 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k + 1 = 1
⊢ k = 0

Tactic:
simp only [add_eq_right] at hk

Premises used: add_eq_right
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
⊢ ζ = -1

Tactic:
IsPrimitiveRoot.eq_neg_one_of_two_right ?_

Premises used: IsPrimitiveRoot.eq_neg_one_of_two_right
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
refine : IsPrimitiveRoot ζ 2
⊢ ζ = -1

Tactic:
refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_

Premises used: IsPrimitiveRoot.eq_neg_one_of_two_right
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
rwa :
  ∀ (hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
    IsPrimitiveRoot ζ 2
rwa₁ :
  ∀ (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 1)) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0),
    IsPrimitiveRoot ζ 2
rwa₂ : ∀ (hζ : IsPrimitiveRoot ζ p) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0), IsPrimitiveRoot ζ 2
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀ (hζ : IsPrimitiveRoot ζ 2) (htwo : p ^ (k + 1) = 2) (hp2 : p = 2) (hk : k = 0), IsPrimitiveRoot ζ 2
⊢ IsPrimitiveRoot ζ 2

Tactic:
rwa [hk, zero_add, pow_one, hp2] at hζ

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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
⊢ ζ = -1

Tactic:
have hζ' : ζ = -1 := by
      refine IsPrimitiveRoot.eq_neg_one_of_two_right ?_
      rwa [hk, zero_add, pow_one, hp2] at hζ
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
h : (↑hζ.toInteger : K) = (↑(-1) : K)
⊢ hζ.toInteger = -1

Tactic:
ext
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
⊢ (↑hζ.toInteger : K) = (↑(-1) : K)

Tactic:
hζ'
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
⊢ (↑hζ.toInteger : K) = (↑(-1) : K)

Tactic:
exact hζ'
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : ζ = -1
⊢ hζ.toInteger = -1

Tactic:
replace hζ' : hζ.toInteger = -1 := by
      ext
      exact hζ'
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
pos : HSub.hSub (α := 𝓞 K) (-1) 1 ∣ (↑2 : 𝓞 K)
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)

Tactic:
rw [hζ', hp2]
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ (↑2 : 𝓞 K) = HSub.hSub (α := 𝓞 K) (-1) 1 * -1

Tactic:
ring
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) = 2
hp2 : p = 2
hk : k = 0
hζ' : hζ.toInteger = -1
⊢ HSub.hSub (α := 𝓞 K) (-1) 1 ∣ (↑2 : 𝓞 K)

Tactic:
exact ⟨-1, by ring⟩
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)

Tactic:
simpa
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
neg : hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)

Tactic:
suffices (hζ.toInteger - 1) ∣ (p : ℤ) by simpa
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
⊢ NumberField K

Tactic:
have := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (β := ℕ) p 0 - 1) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0)

Tactic:
have H := hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two zero_le 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (β := ℕ) p 0 - 1) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1

Tactic:
rw [pow_zero, pow_one] at H

Premises used: pow_zero, 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
neg : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1 ∣ (↑p : ℤ)
neg₁ : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
⊢ hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)

Tactic:
rw [← Ideal.norm_dvd_iff, H]

Premises used: Ideal.norm_dvd_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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1 ∣ (↑p : ℤ)

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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
prime_norm_toInteger_sub_one_of_prime_pow_ne_two hζ htwo

Premises used: IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : ¬p ^ (k + 1) = 2
this : NumberField K
H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
exact prime_norm_toInteger_sub_one_of_prime_pow_ne_two hζ htwo

Premises used: IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_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
hcycl : IsCyclotomicExtension {p} ℚ K
hζ_1 : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ hζ_1.toInteger - 1 ∣ (↑p : 𝓞 K)

Tactic:
toInteger_sub_one_dvd_prime hζ

Premises used: IsPrimitiveRoot.toInteger_sub_one_dvd_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
hcycl : IsCyclotomicExtension {p} ℚ K
hζ_1 : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ hζ_1.toInteger - 1 ∣ (↑p : 𝓞 K)

Tactic:
exact toInteger_sub_one_dvd_prime hζ

Premises used: IsPrimitiveRoot.toInteger_sub_one_dvd_prime
-- 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
h : hζ.toInteger - 1 ∣ 2
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- 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
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)

Tactic:
simp [h]
-- 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
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)

Tactic:
replace h : hζ.toInteger - 1 ∣ (2 : ℤ) := by simp [h]
-- 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 ∣ (↑2 : 𝓞 K)
rw : ∀ (h : Dvd.dvd (α := ℤ) (↑p : ℤ) 2), False
hx : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
⊢ False

Tactic:
rw [← Ideal.norm_dvd_iff, hζ.norm_toInteger_sub_one_of_prime_ne_two hodd] at h

Premises used: Ideal.norm_dvd_iff, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_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))
hodd : p ≠ 2
this : NumberField K
h : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ False

Tactic:
hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_

Premises used: Iff.mp, prime_dvd_prime_iff_eq
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
refine_1 : Prime p
refine_2 : Prime (M := ℕ) 2
refine_3 : p ∣ 2
⊢ False

Tactic:
refine hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_

Premises used: Iff.mp, prime_dvd_prime_iff_eq
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ Prime p

Tactic:
Nat.prime_iff.1 hp.1

Premises used: Nat.prime_iff, 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ Prime p

Tactic:
exact Nat.prime_iff.1 hp.1

Premises used: Nat.prime_iff, 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ Prime (M := ℕ) 2

Tactic:
Nat.prime_iff.1 Nat.prime_two

Premises used: Nat.prime_iff, Nat.prime_two, Iff.mp
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ Prime (M := ℕ) 2

Tactic:
exact Nat.prime_iff.1 Nat.prime_two

Premises used: Nat.prime_iff, Nat.prime_two, Iff.mp
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ p ∣ 2

Tactic:
Int.ofNat_dvd.mp h

Premises used: Int.ofNat_dvd, Iff.mp
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ p ∣ 2

Tactic:
exact Int.ofNat_dvd.mp h

Premises used: Int.ofNat_dvd, Iff.mp
-- 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 ∣ (↑2 : 𝓞 K)
hx : Prime (M := ℤ) (↑p : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
rw [hζ.norm_toInteger_sub_one_of_prime_ne_two hodd]

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_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))
hodd : p ≠ 2
this : NumberField K
h : hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)
⊢ Prime (M := ℤ) (↑p : ℤ)

Tactic:
Nat.prime_iff_prime_int.1 hp.1

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 : hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)
⊢ Prime (M := ℤ) (↑p : ℤ)

Tactic:
exact Nat.prime_iff_prime_int.1 hp.1

Premises used: Nat.prime_iff_prime_int, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
⊢ NeZero n

Tactic:
have : NeZero n := NeZero.of_gt hn
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this : NeZero n
⊢ ∃ (μ : ↥ℚ⟮ζ⟯) (_ : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯) (hμ : IsPrimitiveRoot μ n),
    (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
      HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
⟨IntermediateField.AdjoinSimple.gen ℚ ζ,
      intermediateField_adjoin_isCyclotomicExtension ℚ hζ, coe_submonoidClass_iff.mp hζ, ?_⟩

Premises used: IntermediateField.AdjoinSimple.gen, Rat, IsPrimitiveRoot.coe_submonoidClass_iff, Exists.intro, Iff.mp, IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this : NeZero n
refine :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ ∃ (μ : ↥ℚ⟮ζ⟯) (_ : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯) (hμ : IsPrimitiveRoot μ n),
    (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
      HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)

Tactic:
refine ⟨IntermediateField.AdjoinSimple.gen ℚ ζ,
      intermediateField_adjoin_isCyclotomicExtension ℚ hζ, coe_submonoidClass_iff.mp hζ, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this : NeZero n
⊢ NumberField.{u_1} ↥ℚ⟮ζ⟯

Tactic:
have : NumberField ℚ⟮ζ⟯ := of_intermediateField _
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
hn : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
hp : Dvd.dvd (α := ℤ) ((↑p : ℤ) : ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
this_1 : NeZero n
this : NumberField.{u_1} ↥ℚ⟮ζ⟯
⊢ ζ - 1 = (algebraMap (↥ℚ⟮ζ⟯) K : (a : ↥ℚ⟮ζ⟯) → K) (HSub.hSub (α := ↥ℚ⟮ζ⟯) (AdjoinSimple.gen ℚ ζ) 1)

Tactic:
rfl