awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : NumberField K
H : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) = HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1
neg : HPow.hPow (α := ℤ) (β := ℕ) (↑p : ℤ) 1 ∣ (↑p : ℤ)
⊢ hζ.toInteger - 1 ∣ (↑(↑p : ℤ) : 𝓞 K)
have neg₁ : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
Tactic: rw [← Ideal.norm_dvd_iff, 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ζ.toInteger - 1 ∣ (↑p : 𝓞 K)
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
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} ℚ K
⊢ hζ.toInteger - 1 ∣ (↑p : 𝓞 K)
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))
hodd : p ≠ 2
h : hζ.toInteger - 1 ∣ 2
⊢ False
have this : NumberField K
Tactic: have : NumberField K := IsCyclotomicExtension.numberField {p ^ (k + 1)} ℚ K
-- 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
h : hζ.toInteger - 1 ∣ 2
this : NumberField K
⊢ False
have h₁ : hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)
Tactic: replace h : hζ.toInteger - 1 ∣ (2 : ℤ) := by simp [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
h : hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)
⊢ False
have rw : ∀ (h : Dvd.dvd (α := ℤ) (↑p : ℤ) 2), False
Tactic: rw [← Ideal.norm_dvd_iff, hζ.norm_toInteger_sub_one_of_prime_ne_two hodd] 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
h : hζ.toInteger - 1 ∣ (↑2 : 𝓞 K)
rw : ∀ (h : Dvd.dvd (α := ℤ) (↑p : ℤ) 2), False
⊢ False
have hx : Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
Tactic: rw [← Ideal.norm_dvd_iff, hζ.norm_toInteger_sub_one_of_prime_ne_two hodd] at 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
⊢ False
have refine_1 : Prime p
Tactic: refine hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
refine_1 : Prime p
⊢ False
have refine_2 : Prime (M := ℕ) 2
Tactic: refine hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_
-- 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 : Dvd.dvd (α := ℤ) (↑p : ℤ) 2
refine_1 : Prime p
refine_2 : Prime (M := ℕ) 2
⊢ False
have refine_3 : p ∣ 2
Tactic: refine hodd <| (prime_dvd_prime_iff_eq ?_ ?_).1 ?_
-- 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 ∣ (↑2 : 𝓞 K)
⊢ Prime (M := ℤ) ((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) : ℤ)
have hx : Prime (M := ℤ) (↑p : ℤ)
Tactic: rw [hζ.norm_toInteger_sub_one_of_prime_ne_two hodd]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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) : ℤ)
⊢ p ∣ n
have this : NeZero n
Tactic: have : NeZero n := NeZero.of_gt hn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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)
have refine : (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
  HPow.hPow (α := ℤ)
    ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
        (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
      ℤ)
    (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: refine ⟨IntermediateField.AdjoinSimple.gen ℚ ζ,
      intermediateField_adjoin_isCyclotomicExtension ℚ hζ, coe_submonoidClass_iff.mp hζ, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
have this₁ : NumberField.{u_1} ↥ℚ⟮ζ⟯
Tactic: have : NumberField ℚ⟮ζ⟯ := of_intermediateField _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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} ↥ℚ⟮ζ⟯
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
have rw : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ)
        ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
            (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
          ℤ)
        (Module.finrank (↥ℚ⟮ζ⟯) K)) :
    ℚ)
Tactic: rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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} ↥ℚ⟮ζ⟯
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
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 : ℤ) → ℚ)
      (HPow.hPow (α := ℤ)
        ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
            (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
          ℤ)
        (Module.finrank (↥ℚ⟮ζ⟯) K)) :
    ℚ)
Tactic: rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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} ↥ℚ⟮ζ⟯
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
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 : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
have rw₂ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
    ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ)
        ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
            (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
          ℤ)
        (Module.finrank (↥ℚ⟮ζ⟯) K)) :
    ℚ)
Tactic: rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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} ↥ℚ⟮ζ⟯
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
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 : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₂ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
have rw₃ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 1) : ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ)
        ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
            (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
          ℤ)
        (Module.finrank (↥ℚ⟮ζ⟯) K)) :
    ℚ)
Tactic: rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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} ↥ℚ⟮ζ⟯
rw :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (hζ.toInteger - 1) : K) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
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 : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₂ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HSub.hSub (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) hζ.toInteger : K) (1 : K)) :
      ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
rw₃ :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) (ζ - 1) : ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (HPow.hPow (α := ℤ)
          ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
              (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
            ℤ)
          (Module.finrank (↥ℚ⟮ζ⟯) K)) :
      ℚ)
⊢ (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ)
      ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
          (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) ⋯) 1) :
        ℤ)
      (Module.finrank (↥ℚ⟮ζ⟯) K)
have rw₄ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      ((algebraMap (↥ℚ⟮ζ⟯) K : (a : ↥ℚ⟮ζ⟯) → K) (HSub.hSub (α := ↥ℚ⟮ζ⟯) (AdjoinSimple.gen ℚ ζ) 1) : K) :
    ℚ)
  ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
      (HPow.hPow (α := ℤ)
        ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ)
            (HSub.hSub (α := 𝓞 ↥ℚ⟮ζ⟯) (toInteger (ζ := AdjoinSimple.gen ℚ ζ) (k := n) sorry) 1) :
          ℤ)
        (Module.finrank (↥ℚ⟮ζ⟯) K)) :
    ℚ)
Tactic: rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
⊢ p ∣ n
have obtain : ∀ (μ : ↥ℚ⟮ζ⟯) (hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯) (hμ : IsPrimitiveRoot μ n)
  (h :
    (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
      HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)),
  p ∣ n
Tactic: obtain ⟨μ, hC, hμ, h⟩ :
      ∃ μ : ℚ⟮ζ⟯, ∃ (_ : IsCyclotomicExtension {n} ℚ ℚ⟮ζ⟯), ∃ (hμ : IsPrimitiveRoot μ n),
      norm ℤ (hζ.toInteger - 1) = norm ℤ (hμ.toInteger - 1) ^ Module.finrank ℚ⟮ζ⟯ K := by
    refine ⟨IntermediateField.AdjoinSimple.gen ℚ ζ,
      intermediateField_adjoin_isCyclotomicExtension ℚ hζ, coe_submonoidClass_iff.mp hζ, ?_⟩
    have : NumberField ℚ⟮ζ⟯ := of_intermediateField _
    rw [norm_eq_iff ℤ (Sₘ := K) (Rₘ := ℚ) le_rfl, map_sub, map_one, RingOfIntegers.map_mk,
      show ζ - 1 = algebraMap ℚ⟮ζ⟯ K (IntermediateField.AdjoinSimple.gen ℚ ζ - 1) by rfl,
      ← norm_norm (S := ℚ⟮ζ⟯), Algebra.norm_algebraMap, map_pow, map_pow, ← norm_localization ℤ
      (nonZeroDivisors ℤ) (Sₘ := ℚ⟮ζ⟯), map_sub (algebraMap _ _), RingOfIntegers.map_mk, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ p ∣ n
have hp₁ : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: rw [h] at hp
Cleared hypotheses: hp, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have inl : ∀ (hn : 2 < n), ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: obtain hn | hn := lt_or_eq_of_le hn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
inl :
  ∀ (hn : 2 < n),
    ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have inr : ∀ (hn : 2 = n), ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: obtain hn | hn := lt_or_eq_of_le hn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn_1 : 2 ≤ n
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : K
p : ℕ
hF : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ n
this : NeZero n
μ : ↥ℚ⟮ζ⟯
hC : IsCyclotomicExtension.{0, u_1} {n} ℚ ↥ℚ⟮ζ⟯
hμ : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have pos : ∀ (h : ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ), q ^ t = n),
  ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: by_cases! h : ∃ q, q.Prime ∧ ∃ t, q ^ t = n