awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : NumberField K
this : NeZero n
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)
rw₁ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)
rw₂ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 1 : ℚ)
rw₃ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    (1 : ℚ)
rw₄ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 1) : ℚ) (1 : ℚ)
rw₅ : Eq (α := ℚ) (↑(eval 1 (cyclotomic n ℤ)) : ℚ) 1
rw₆ : Eq (α := ℚ) (↑1 : ℚ) 1
rw₇ rw₈ : Eq (α := ℚ) 1 1
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)

Tactic:
rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, map_one, RingOfIntegers.map_mk,
    sub_one_norm_eq_eval_cyclotomic hζ h₁ (cyclotomic.irreducible_rat (NeZero.pos _)),
    eval_one_cyclotomic_not_prime_pow h₂, Int.cast_one]

Premises used: le_rfl, map_sub, Algebra.norm_eq_iff, Int, IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic, Polynomial.eval_one_cyclotomic_not_prime_pow, map_one, Polynomial.cyclotomic.irreducible_rat, NeZero.pos, NumberField.RingOfIntegers.map_mk, Int.cast_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))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 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))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger ^ p ^ s - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)) : ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ p ^ s - 1) = HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)

Tactic:
rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]

Premises used: le_rfl, Algebra.norm_eq_iff, 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))
s : ℕ
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
this : NumberField K
⊢ Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger ^ p ^ s - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)) : ℚ)

Tactic:
simp [hζ.norm_pow_sub_one_of_prime_pow_ne_two (cyclotomic.irreducible_rat (NeZero.pos _)) hs htwo]

Premises used: IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_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 : NumberField K := 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
rw :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger ^ HPow.hPow (α := ℕ) 2 k - 1) : K) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (-2) (HPow.hPow (α := ℕ) 2 k)) : ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (α := ℕ) 2 k - 1) =
    HPow.hPow (α := ℤ) (-2) (HPow.hPow (α := ℕ) 2 k)

Tactic:
rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]

Premises used: le_rfl, Algebra.norm_eq_iff, Int
-- 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
⊢ LT.lt (α := ℕ) 0 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
⊢ Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger ^ HPow.hPow (α := ℕ) 2 k - 1) : K) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (HPow.hPow (α := ℤ) (-2) (HPow.hPow (α := ℕ) 2 k)) : ℚ)

Tactic:
simp [hζ.norm_pow_sub_one_two (cyclotomic.irreducible_rat (pow_pos (by decide) _))]

Premises used: pow_pos, IsPrimitiveRoot.norm_pow_sub_one_two, Polynomial.cyclotomic.irreducible_rat
-- 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))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ p ^ s - 1) = HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)

Tactic:
hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two hs (fun h ↦ hodd ?_)

Premises used: IsPrimitiveRoot.norm_toInteger_pow_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
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
refine : ∀ (h : p ^ (k - s + 1) = 2), p = 2
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ p ^ s - 1) = HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)

Tactic:
refine hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two hs (fun h ↦ hodd ?_)

Premises used: IsPrimitiveRoot.norm_toInteger_pow_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
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
apply : p ^ (k - s).succ = HPow.hPow (α := ℕ) (β := ℕ) 2 1
apply₁ : ℕ
⊢ p = 2

Tactic:
apply eq_of_prime_pow_eq hp.out.prime Nat.prime_two.prime (k - s).succ_pos

Premises used: HSub.hSub, Nat.Prime.prime, eq_of_prime_pow_eq, Nat.prime_two, Nat.succ_pos, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u_1
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 2)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 2))
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {2 ^ (k + 2)} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
k : ℕ
K : Type u_1
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 2)} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 2))
this : NumberField K
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)
rw₁ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)
rw₂ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)
rw₃ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    ((↑2 : ℚ) : ℚ)
rw₄ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    (2 : ℚ)
rw₅ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 1) : ℚ) (2 : ℚ)
rw₆ rw₇ : Eq (α := ℚ) 2 2
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)

Tactic:
rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, eq_intCast, Int.cast_ofNat,
    RingOfIntegers.map_mk, hζ.norm_sub_one_two (Nat.le_add_left 2 k)
    (Polynomial.cyclotomic.irreducible_rat (Nat.two_pow_pos _))]

Premises used: le_rfl, map_sub, Nat.le_add_left, Nat.two_pow_pos, Algebra.norm_eq_iff, Int, eq_intCast, Int.cast_ofNat, map_one, Polynomial.cyclotomic.irreducible_rat, NumberField.RingOfIntegers.map_mk, OfNat.ofNat, 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))
hodd : p ≠ 2
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
simpa only [pow_zero, pow_one] using
    hζ.norm_toInteger_pow_sub_one_of_prime_ne_two (Nat.zero_le _) hodd

Premises used: Nat.zero_le, pow_zero, pow_one, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {2} ℚ K
hζ : IsPrimitiveRoot ζ 2
⊢ 2 = HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1)

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

Tactic:
rw [show 2 = (2 ^ (0 + 1)) by norm_num] at hζ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {2} ℚ K
hζ_1 : IsPrimitiveRoot ζ 2
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) (-2 : ℤ)

Tactic:
simpa using hζ.norm_toInteger_pow_sub_one_of_two

Premises used: IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_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ζ : IsPrimitiveRoot ζ p
h : p ≠ 2
⊢ 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
h : p ≠ 2
⊢ 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
h : p ≠ 2
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
h : p ≠ 2
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
h : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
hζ.norm_toInteger_sub_one_of_prime_ne_two h

Premises used: IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_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
h : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
exact hζ.norm_toInteger_sub_one_of_prime_ne_two h

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))
htwo : p ^ (k + 1) ≠ 2
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (β := ℕ) p 0 - 1) =
    HPow.hPow (α := ℤ) (↑p : ℤ) (HPow.hPow (β := ℕ) p 0)

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

Tactic:
simp only [pow_zero, pow_one] at this

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
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
rw : Prime (M := ℤ) (↑p : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
rw [this]
-- 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 ^ (k + 1) ≠ 2
this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ 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))
htwo : p ^ (k + 1) ≠ 2
this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ Prime (M := ℤ) (↑p : ℤ)

Tactic:
exact 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)

Tactic:
have := hζ.norm_toInteger_sub_one_of_prime_ne_two hodd
-- 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))
hodd : p ≠ 2
this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
rw : Prime (M := ℤ) (↑p : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)

Tactic:
rw [this]
-- 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))
hodd : p ≠ 2
this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hodd : p ≠ 2
this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
⊢ Prime (M := ℤ) (↑p : ℤ)

Tactic:
exact 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 : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
⊢ 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
hodd : p ≠ 2
⊢ 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
hodd : p ≠ 2
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
hodd : p ≠ 2
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
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ)

Tactic:
hζ.prime_norm_toInteger_sub_one_of_prime_ne_two hodd

Premises used: IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_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
hodd : p ≠ 2
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ_1.toInteger - 1) : ℤ)

Tactic:
exact hζ.prime_norm_toInteger_sub_one_of_prime_ne_two hodd

Premises used: IsPrimitiveRoot.prime_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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ pB.dim = p ^ k * (p - 1)

Tactic:
simp [integralPowerBasisOfPrimePow_dim, pB, Nat.totient_prime_pow hp.1 (Nat.zero_lt_succ k)]

Premises used: Nat.totient_prime_pow, Nat.zero_lt_succ, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, 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
hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
htwo : p ^ (k + 1) ≠ 2
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
⊢ pB.dim = p ^ k * (p - 1)

Tactic:
have hdim : pB.dim = p ^ k * (↑p - 1) := by
    simp [integralPowerBasisOfPrimePow_dim, pB, Nat.totient_prime_pow hp.1 (Nat.zero_lt_succ 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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
rw : p ^ k * (p - 1) ≠ 0 ∧ p ^ k * (p - 1) ≠ 1
⊢ 1 < pB.dim

Tactic:
rw [Nat.one_lt_iff_ne_zero_and_ne_one, hdim]

Premises used: Nat.one_lt_iff_ne_zero_and_ne_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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
⊢ p ^ k * (p - 1) ≠ 0

Tactic:
simp only [ne_eq, mul_eq_zero, NeZero.ne _, Nat.sub_eq_zero_iff_le, false_or,
      not_le, Nat.Prime.one_lt hp.out]

Premises used: not_le, Nat.Prime.one_lt, Nat.sub_eq_zero_iff_le, false_or, mul_eq_zero, ne_eq, Fact.out, NeZero.ne
-- 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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
refine : 1 < p ^ k * (p - 1)
⊢ p ^ k * (p - 1) ≠ 0 ∧ p ^ k * (p - 1) ≠ 1

Tactic:
refine ⟨by simp only [ne_eq, mul_eq_zero, NeZero.ne _, Nat.sub_eq_zero_iff_le, false_or,
      not_le, Nat.Prime.one_lt hp.out], ne_of_gt ?_⟩
-- 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
n : ℤ
x : 𝓞 K
h : hζ.toInteger - (↑n : 𝓞 K) = (↑p : 𝓞 K) * x
pB : PowerBasis ℤ (𝓞 K) := hζ.integralPowerBasisOfPrimePow
hdim : pB.dim = p ^ k * (p - 1)
pos : ∀ (hk : k = 0), 1 < p ^ k * (p - 1)
neg : ∀ (hk : ¬k = 0), 1 < p ^ k * (p - 1)
⊢ 1 < p ^ k * (p - 1)

Tactic:
by_cases hk : k = 0