awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
⊢ Membership.mem (γ := Subalgebra ℤ (𝓞 K))
    ℤ[Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) ⋯]
    hζ.integralPowerBasisOfPrimePow.gen
have h : hζ.integralPowerBasisOfPrimePow.gen =
  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra ℤ K) (integralClosure ℤ K) x) (ζ - 1) sorry + 1
Tactic: convert! Subalgebra.add_mem _ (self_mem_adjoin_singleton ℤ _) (Subalgebra.one_mem _)
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Prime (hζ.toInteger - 1)
have refine_1 : ∀ (h : hζ.toInteger - 1 = 0), False
Tactic: refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
refine_1 : ∀ (h : hζ.toInteger - 1 = 0), False
⊢ Prime (hζ.toInteger - 1)
have refine_2 : Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)
Tactic: refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
h : hζ.toInteger - 1 = 0
⊢ False
have refine_1 : HPow.hPow (β := ℕ) ζ 1 = 1
Tactic: apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ hp.out.one_lt (by simp))
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
h : hζ.toInteger - 1 = 0
⊢ HPow.hPow (β := ℕ) ζ 1 = 1
have h₁ : hζ.toInteger = 1
Tactic: rw [sub_eq_zero] at h
Cleared hypotheses: h
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)
have refine_2 : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
Tactic: rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
    ← Int.prime_iff_natAbs_prime]
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have h : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
Tactic: convert! Nat.prime_iff_prime_int.1 hp.out
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) ((↑p : ℤ) : ℤ)
have h : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ)
Tactic: apply RingHom.injective_int (algebraMap ℤ ℚ)
-- 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))
hodd : p ≠ 2
this : NumberField K := ⋯
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ)
have h : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑p : ℤ) : ℚ)
Tactic: rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
-- 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))
⊢ Prime (hζ.toInteger - 1)
have this : NumberField K
Tactic: have := 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
⊢ Prime (hζ.toInteger - 1)
have refine_1 : ∀ (h : hζ.toInteger - 1 = 0), False
Tactic: refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
-- 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
refine_1 : ∀ (h : hζ.toInteger - 1 = 0), False
⊢ Prime (hζ.toInteger - 1)
have refine_2 : Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)
Tactic: refine Ideal.prime_of_irreducible_absNorm_span (fun h ↦ ?_) ?_
-- 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
h : hζ.toInteger - 1 = 0
⊢ False
have refine_1 : HPow.hPow (β := ℕ) ζ 1 = 1
Tactic: apply hζ.pow_ne_one_of_pos_of_lt one_ne_zero (one_lt_pow₀ (by decide) (by simp))
-- 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))
this : NumberField K
h : hζ.toInteger - 1 = 0
⊢ HPow.hPow (β := ℕ) ζ 1 = 1
have h₁ : hζ.toInteger = 1
Tactic: rw [sub_eq_zero] at h
Cleared hypotheses: h
-- 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
⊢ Irreducible (M := ℕ) ((Ideal.absNorm : (a : Ideal (𝓞 K)) → ℕ) (Ideal.span {hζ.toInteger - 1}) : ℕ)
have refine_2 : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
Tactic: rw [Nat.irreducible_iff_prime, Ideal.absNorm_span_singleton, ← Nat.prime_iff,
    ← Int.prime_iff_natAbs_prime]
-- 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
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have 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) : ℤ)
Tactic: cases k
Cleared hypotheses: k, inst_2, hζ
-- 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
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) : ℤ)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have 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) : ℤ)
Tactic: cases k
Cleared hypotheses: k, inst_2, hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have h : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (-2 : ℤ)
Tactic: convert! Prime.neg Int.prime_two
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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) → ℤ) (hζ.toInteger - 1) : ℤ) (-2 : ℤ)
have h : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (-2) : ℚ)
Tactic: apply RingHom.injective_int (algebraMap ℤ ℚ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (-2) : ℚ)
have h : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (-2) : ℚ)
Tactic: rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have h : Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
Tactic: convert! Int.prime_two
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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) → ℤ) (hζ.toInteger - 1) : ℤ) (2 : ℤ)
have h : Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)
Tactic: apply RingHom.injective_int (algebraMap ℤ ℚ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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 (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 2 : ℚ)
have h : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
  ((Int.castRingHom ℚ : (a : ℤ) → ℚ) 2 : ℚ)
Tactic: rw [← Algebra.norm_localization (Sₘ := K) ℤ (nonZeroDivisors ℤ), algebraMap_int_eq]
-- 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))
⊢ Prime (hζ.toInteger - 1)
have pos : ∀ (htwo : p = 2), Prime (hζ.toInteger - 1)
Tactic: by_cases htwo : p = 2
-- 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))
pos : ∀ (htwo : p = 2), Prime (hζ.toInteger - 1)
⊢ Prime (hζ.toInteger - 1)
have neg : ∀ (htwo : ¬p = 2), Prime (hζ.toInteger - 1)
Tactic: by_cases htwo : p = 2
-- 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 = 2
⊢ Prime (hζ.toInteger - 1)
have hp₁ : Fact (Nat.Prime 2)
Tactic: subst htwo
Cleared hypotheses: p, hp, inst_2, hζ, 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 = 2
hp₁ : Fact (Nat.Prime 2)
⊢ Prime (hζ.toInteger - 1)
have inst : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} ℚ K
Tactic: subst htwo
Cleared hypotheses: p, hp, inst_2, hζ, htwo
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Prime (hζ.toInteger - 1)
have hζ₁ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
Tactic: subst htwo
Cleared hypotheses: p, hp, inst_3, hζ, htwo
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ Prime (hζ.toInteger - 1)
have convert! : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
Tactic: convert! zeta_sub_one_prime (k := 0) (by simpa only [zero_add, pow_one])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ have this : NeZero n := ⋯;
  Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ have this : NeZero n := ⋯;
  Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have this₁ : NeZero n
Tactic: have : NeZero n := NeZero.of_gt h₁
-- 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
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
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 : ℤ) → ℚ) 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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw₂ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
    ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) 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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw₃ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
    ℚ)
  (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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw₄ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 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 : ℚ)
⊢ Eq (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ) (1 : ℤ)
have rw₅ : Eq (α := ℚ) (↑(eval 1 (cyclotomic n ℤ)) : ℚ) 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]