awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw₆ : Eq (α := ℚ) (↑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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw₇ : Eq (α := ℚ) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ p ^ s - 1) = HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ p ^ s - 1) = HPow.hPow (α := ℤ) (↑p : ℤ) (p ^ s)
have 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)) : ℚ)
Tactic: rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (α := ℕ) 2 k - 1) =
    HPow.hPow (α := ℤ) (-2) (HPow.hPow (α := ℕ) 2 k)
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {2 ^ (k + 1)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger ^ HPow.hPow (α := ℕ) 2 k - 1) =
    HPow.hPow (α := ℤ) (-2) (HPow.hPow (α := ℕ) 2 k)
have 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)) : ℚ)
Tactic: rw [Algebra.norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
have refine : ∀ (h : p ^ (k - s + 1) = 2), p = 2
Tactic: refine hζ.norm_toInteger_pow_sub_one_of_prime_pow_ne_two hs (fun h ↦ hodd ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ p = 2
have apply : p ^ (k - s).succ = HPow.hPow (α := ℕ) (β := ℕ) 2 1
Tactic: apply eq_of_prime_pow_eq hp.out.prime Nat.prime_two.prime (k - s).succ_pos
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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))
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {2 ^ (k + 2)} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have rw : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have 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 : ℚ)
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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have rw₂ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
    ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have rw₃ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
    ℚ)
  ((↑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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 : ℚ) : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have rw₄ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
    ℚ)
  (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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have rw₅ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have rw₆ : Eq (α := ℚ) 2 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 _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
K : Type u
inst : Field K
ζ : K
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {2} ℚ K
hζ : IsPrimitiveRoot ζ 2
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (-2 : ℤ)
have hζ₁ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1))
Tactic: rw [show 2 = (2 ^ (0 + 1)) by norm_num] at hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
Tactic: have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have hζ₁ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have this : (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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have this₁ : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: simp only [pow_zero, pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have rw : Prime (M := ℤ) (↑p : ℤ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have this : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: have := hζ.norm_toInteger_sub_one_of_prime_ne_two hodd
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have rw : Prime (M := ℤ) (↑p : ℤ)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
Tactic: have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have hζ₁ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ False
have hdim : 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
⊢ 1 < pB.dim
have rw : p ^ k * (p - 1) ≠ 0 ∧ p ^ k * (p - 1) ≠ 1
Tactic: rw [Nat.one_lt_iff_ne_zero_and_ne_one, hdim]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 ∧ p ^ k * (p - 1) ≠ 1
have refine : 1 < p ^ k * (p - 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 ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
⊢ 1 < p ^ k * (p - 1)
have pos : ∀ (hk : k = 0), 1 < p ^ k * (p - 1)
Tactic: by_cases hk : k = 0