awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have neg : ∀ (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
-- 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_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
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
have pos : ∀ (q : ℕ) (hq : Nat.Prime q) (t : ℕ) (hn' : q ^ t = n),
  ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: obtain ⟨q, hq, t, hn'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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 : ℕ
hq : Nat.Prime q
t : ℕ
hn' : q ^ t = n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have this₁ : Fact (Nat.Prime q)
Tactic: have : Fact (Nat.Prime q) := ⟨hq⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : 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 : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hn' : q ^ (r + 1) = n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have hμ₁ : IsPrimitiveRoot μ (q ^ (r + 1))
Tactic: rw [← hn'] at hC hμ
Cleared hypotheses: hC, hn'
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : 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 : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hn' : q ^ (r + 1) = n
hμ₁ : IsPrimitiveRoot μ (q ^ (r + 1))
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have hC₁ : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
Tactic: rw [← hn'] at hC hμ
Cleared hypotheses: hC, 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have pos : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
-- 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have pos : ∀ (hq' : q = 2), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: by_cases hq' : q = 2
-- 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
pos : ∀ (hq' : q = 2), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have neg : ∀ (hq' : ¬q = 2), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: by_cases hq' : q = 2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1)
hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have hn₁ : LT.lt (α := ℕ) 2 2
Tactic: rw [← hn', hq', zero_add, pow_one] at hn
Cleared hypotheses: hn, hq, this, hq', hμ, hC, 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
k : ℕ
hμ : IsPrimitiveRoot μ (q ^ (k + 1 + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (k + 1 + 1) = n
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have pos : ∀ (hμ : IsPrimitiveRoot μ (HPow.hPow (α := ℕ) 2 (k + 1 + 1)))
  (hC : IsCyclotomicExtension.{0, u_1} {HPow.hPow (α := ℕ) 2 (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ (k + 1 + 1) = n),
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: rw [hq'] at hC hμ ⊢
Cleared hypotheses: hμ, hC, 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
hq' : q = 2
k : ℕ
hμ : IsPrimitiveRoot μ (HPow.hPow (α := ℕ) 2 (k + 1 + 1))
hC : IsCyclotomicExtension.{0, u_1} {HPow.hPow (α := ℕ) 2 (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (k + 1 + 1) = n
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have pos : ∀ (hp : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) 2 (Module.finrank (↥ℚ⟮ζ⟯) K))
  (h :
    (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
      HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K))
  (hn : 2 < n) (q : ℕ) (hq : Nat.Prime q) (this : Fact (Nat.Prime q)) (hq' : q = 2) (k : ℕ)
  (hμ : IsPrimitiveRoot μ (HPow.hPow (α := ℕ) 2 (k + 1 + 1)))
  (hC : IsCyclotomicExtension.{0, u_1} {HPow.hPow (α := ℕ) 2 (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ (k + 1 + 1) = n),
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
Cleared hypotheses: hp, h, hn, q, hq, this, hq', k, hμ, hC, 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : q = 2
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have pos : ∀ (hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1))
  (hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n),
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
Cleared hypotheses: r, hμ, hC, 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : q = 2
pos :
  ∀ (hμ : IsPrimitiveRoot μ (q ^ HAdd.hAdd (α := ℕ) 0 1))
    (hC : IsCyclotomicExtension.{0, u_1} {q ^ HAdd.hAdd (α := ℕ) 0 1} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ HAdd.hAdd (α := ℕ) 0 1 = n),
    (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have pos₁ : ∀ (k : ℕ) (hμ : IsPrimitiveRoot μ (q ^ (k + 1 + 1))) (hC : IsCyclotomicExtension.{0, u_1} {q ^ (k + 1 + 1)} ℚ ↥ℚ⟮ζ⟯)
  (hn' : q ^ (k + 1 + 1) = n), (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
Cleared hypotheses: r, hμ, hC, 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_1 : NeZero n
μ : ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
q : ℕ
hq : Nat.Prime q
this : Fact (Nat.Prime q)
r : ℕ
hμ : IsPrimitiveRoot μ (q ^ (r + 1))
hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯
hn' : q ^ (r + 1) = n
hq' : ¬q = 2
⊢ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
have neg : ∀ (hp : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)) (hq : Nat.Prime q)
  (this : Fact (Nat.Prime q)) (r : ℕ) (hμ : IsPrimitiveRoot μ (q ^ (r + 1)))
  (hC : IsCyclotomicExtension.{0, u_1} {q ^ (r + 1)} ℚ ↥ℚ⟮ζ⟯) (hn' : q ^ (r + 1) = n) (hq' : ¬q = 2),
  (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
Cleared hypotheses: hp, hq, this, r, hμ, hC, hn', hq'
-- 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_1 : 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 : ℕ
hq : Nat.Prime q
t : ℕ
hn' : q ^ t = n
this : Fact (Nat.Prime q)
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have pos : ∀ (hn' : HPow.hPow (β := ℕ) q 0 = n),
  ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
Cleared hypotheses: t, 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_1 : 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 : ℕ
hq : Nat.Prime q
t : ℕ
hn' : q ^ t = n
this : Fact (Nat.Prime q)
pos :
  ∀ (hn' : HPow.hPow (β := ℕ) q 0 = 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 pos₁ : ∀ (r : ℕ) (hn' : q ^ (r + 1) = n),
  ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ n = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: cases t with
        | zero => simp [← hn'] at hn
        | succ r =>
          rw [← hn'] at hC hμ
          refine ⟨q, hq, r + 1, Module.finrank (ℚ⟮ζ⟯) K, r.add_one_ne_zero, hn'.symm, ?_⟩
          by_cases hq' : q = 2
          · cases r with
            | zero =>
                rw [← hn', hq', zero_add, pow_one] at hn
                exact hn.false.elim
            | succ k =>
                rw [hq'] at hC hμ ⊢
                rwa [hμ.norm_toInteger_sub_one_of_eq_two_pow] at hp
          · rwa [hμ.norm_toInteger_sub_one_of_prime_ne_two hq'] at hp
Cleared hypotheses: t, 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_1 :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 < n
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
have neg : ∀ (hp : p = 1)
  (h :
    (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
      HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K))
  (hn : 2 < n) (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: rw [IsPrimitiveRoot.norm_toInteger_sub_one_eq_one hμ hn, one_pow,
          Int.natCast_dvd_ofNat, Nat.dvd_one] at hp
Cleared hypotheses: hp, h_1, hn, h
-- 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 inr : ∀ (hC : IsCyclotomicExtension.{0, u_1} {2} ℚ ↥ℚ⟮ζ⟯) (hμ : IsPrimitiveRoot μ n) (hμ_1 : IsPrimitiveRoot μ 2)
  (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 ∧ 2 = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
Tactic: rw [← hn] at hμ hC ⊢
Cleared hypotheses: hC, hμ, hp, h, 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} {2} ℚ ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 = n
⊢ 2 = HPow.hPow (α := ℕ) (β := ℕ) 2 1
have rw : Eq (α := ℕ) 2 2
Tactic: rw [pow_one]
-- 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} {2} ℚ ↥ℚ⟮ζ⟯
hμ_1 : IsPrimitiveRoot μ n
hμ : IsPrimitiveRoot μ 2
hp :
  (↑p : ℤ) ∣
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
h :
  (Algebra.norm ℤ : (a : 𝓞 K) → ℤ) (hζ.toInteger - 1) =
    HPow.hPow (α := ℤ) ((Algebra.norm ℤ : (a : 𝓞 ↥ℚ⟮ζ⟯) → ℤ) (hμ_1.toInteger - 1) : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
hn : 2 = n
⊢ ∃ (q : ℕ), Nat.Prime q ∧ ∃ (t : ℕ) (s : ℕ), t ≠ 0 ∧ 2 = q ^ t ∧ (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑q : ℤ) s
have inr : (↑p : ℤ) ∣ HPow.hPow (α := ℤ) (↑2 : ℤ) (Module.finrank (↥ℚ⟮ζ⟯) K)
Tactic: refine ⟨2, Nat.prime_two, 1, Module.finrank ℚ⟮ζ⟯ K, one_ne_zero, by rw [pow_one], ?_⟩