awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : Module.finrank.{u, v} K ↥K⟮η⟯ * Module.finrank (↥K⟮η⟯) L = Module.finrank K L
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
have this₁ : (p - 1) * (p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L) = (p - 1) * p ^ (k.succ - 1)
Tactic: rw [IsCyclotomicExtension.finrank L hirr, IsCyclotomicExtension.finrank K⟮η⟯ hirr₁,
    Nat.totient_prime_pow hpri.out (k - s).succ_pos, Nat.totient_prime_pow hpri.out k.succ_pos,
    mul_comm _ (p - 1), mul_assoc, mul_comm (p ^ (k.succ - 1))] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : (p - 1) * (p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L) = (p - 1) * p ^ (k.succ - 1)
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
have this₁ : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
Tactic: replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ k.succ - 1 = (k - s).succ - 1 + s
have simp : k = k - s + s
Tactic: simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
have Hex : k.succ - 1 = (k - s).succ - 1 + s
Tactic: have Hex : k.succ - 1 = (k - s).succ - 1 + s := by
    simp only [Nat.succ_sub_succ_eq_sub, tsub_zero]
    exact (Nat.sub_add_cancel hs).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
htwo : p ^ (k - s + 1) ≠ 2
hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ (k - s + 1)) K)
η : L := ζ ^ p ^ s - 1
η₁ : ↥K⟮η⟯ := IntermediateField.AdjoinSimple.gen K η
this_1 : IsCyclotomicExtension.{u, v} {p ^ (k - s + 1)} K ↥K⟮η⟯
hη : IsPrimitiveRoot (η₁ + 1) (p ^ (k - s + 1))
this_2 : FiniteDimensional K L
this_3 : IsGalois K L
H : Eq.{u + 1} (α := K) ((Algebra.norm K : (a : ↥K⟮η⟯) → K) η₁ : K) ((↑(p ^ (k - s + 1)).minFac : K) : K)
this : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ (k.succ - 1)
Hex : k.succ - 1 = (k - s).succ - 1 + s
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s
have this₁ : p ^ ((k - s).succ - 1) * Module.finrank (↥K⟮η⟯) L = p ^ ((k - s).succ - 1) * p ^ s
Tactic: rw [Hex, pow_add] at this
Cleared hypotheses: this, Hex
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have refine : ∀ (h : p ^ (k - s + 1) = 2), False
Tactic: refine hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs fun h => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = 2
⊢ False
have h₁ : p ^ (k - s + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
Tactic: rw [← pow_one 2] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
s : ℕ
hs : s ≤ k
hodd : p ≠ 2
h : p ^ (k - s + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1
⊢ False
have h₁ : p = 2
Tactic: replace h :=
    eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (k - s).succ_pos h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ p
hirr : Irreducible (M := K[X]) (cyclotomic p K)
h : p ≠ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑p : K) : K)
have hirr₁ : Irreducible (M := K[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) K)
Tactic: replace hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K) := by simp [hirr]
Cleared hypotheses: hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
hζ : IsPrimitiveRoot ζ p
h : p ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑p : K) : K)
have hζ₁ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
Tactic: replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simp [hζ]
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
hpri : Fact (Nat.Prime p)
hcyc : IsCyclotomicExtension {p} K L
h : p ≠ 2
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) K)
hζ : IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑p : K) : K)
have this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
Tactic: haveI : IsCyclotomicExtension {p ^ (0 + 1)} K L := by simp [hcyc]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)
have this : IsPrimitiveRoot (ζ ^ HPow.hPow (α := ℕ) 2 k) (HPow.hPow (α := ℕ) 2 (k + 1) / HPow.hPow (α := ℕ) 2 k)
Tactic: have := hζ.pow_of_dvd
    (fun h => two_ne_zero (eq_zero_of_pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k))
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ HPow.hPow (α := ℕ) 2 k) (HPow.hPow (α := ℕ) 2 (k + 1) / HPow.hPow (α := ℕ) 2 k)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)
have this₁ : IsPrimitiveRoot (ζ ^ HPow.hPow (α := ℕ) 2 k) 2
Tactic: rw [Nat.pow_div (le_succ k) zero_lt_two, Nat.succ_sub (le_refl k), Nat.sub_self, pow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ HPow.hPow (α := ℕ) 2 k) 2
⊢ HSub.hSub (α := L) (-1) 1 = (algebraMap K L : (a : K) → L) (-2)
have simp : HSub.hSub (α := L) (-1) 1 = -2
Tactic: simp only [map_neg, map_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ HPow.hPow (α := ℕ) 2 k) 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)
have H : HSub.hSub (α := L) (-1) 1 = (algebraMap K L : (a : K) → L) (-2)
Tactic: have H : (-1 : L) - (1 : L) = algebraMap K L (-2) := by
    simp only [map_neg, map_ofNat]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
inst_3 : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ HPow.hPow (α := ℕ) 2 k) 2
H : HSub.hSub (α := L) (-1) 1 = (algebraMap K L : (a : K) → L) (-2)
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)
have rw : HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1) =
  HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)
Tactic: rw [this.eq_neg_one_of_two_right, H, Algebra.norm_algebraMap,
    IsCyclotomicExtension.finrank L hirr, totient_prime_pow Nat.prime_two (zero_lt_succ k),
    succ_sub_succ_eq_sub, tsub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 k)
hk : 2 ≤ k
H : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 k} K L
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) (2 : K)
have this : 2 < HPow.hPow (α := ℕ) 2 k
Tactic: have : 2 < 2 ^ k := by
    nth_rw 1 [← pow_one 2]
    exact Nat.pow_lt_pow_right one_lt_two (lt_of_lt_of_le one_lt_two hk)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k : ℕ
hk : 2 ≤ k
H : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 k} K L
this : 2 < HPow.hPow (α := ℕ) 2 k
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 k)
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) (2 : K)
have obtain : ∀ (k₁ : ℕ) (hk₁ : k = k₁.succ), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) (2 : K)
Tactic: obtain ⟨k₁, hk₁⟩ := exists_eq_succ_of_ne_zero (lt_of_lt_of_le zero_lt_two hk).ne.symm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have pos : ∀ (htwo : p ^ (k - s + 1) = 2), (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
Tactic: by_cases htwo : p ^ (k - s + 1) = 2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
pos :
  ∀ (htwo : p ^ (k - s + 1) = 2), (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have neg : ∀ (htwo : ¬p ^ (k - s + 1) = 2), (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
Tactic: by_cases htwo : p ^ (k - s + 1) = 2
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hp : p = 2
Tactic: obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hks : k - s + 1 = 1
Tactic: obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s + 1 = 1
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hks₁ : k - s = 0
Tactic: simp only [add_eq_right] at hks
Cleared hypotheses: hks
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (hypothesis)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have hs₁ : s = k
Tactic: replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hpri : Fact (Nat.Prime p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (M := K[X]) (cyclotomic (p ^ (k + 1)) K)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)
have pos : ∀ (hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1)))
  (hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K))
  (hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L),
  (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 k)
Tactic: simp only [hp, hs] at hζ hirr hcycl ⊢
Cleared hypotheses: hζ, hcycl, hirr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 k)
have pos : ∀ (k₁ : ℕ) (hk₁ : k = k₁.succ),
  (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 k)
Tactic: obtain ⟨k₁, hk₁⟩ := Nat.exists_eq_succ_of_ne_zero hk
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots (goal)
Goal:
p : ℕ
K : Type u
L : Type v
inst : Field L
ζ : L
inst_1 : Field K
inst_2 : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hks : k - s = 0
hs : s = k
hζ : IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 (k + 1))
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)
hcycl : IsCyclotomicExtension {HPow.hPow (α := ℕ) 2 (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 1) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 k)
have pos : HPow.hPow (α := K) 2 (HPow.hPow (α := ℕ) 2 (k₁ + 1)) = HPow.hPow (α := K) (↑2 : K) (HPow.hPow (α := ℕ) 2 (k₁ + 1))
Tactic: rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,
      mul_pow, neg_one_sq, one_mul, ← pow_mul, ← _root_.pow_succ']
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
f : (α → ℕ) → ℤ
⊢ IsPoly f → IsPoly (-f)
have rw : IsPoly f → IsPoly (0 - f)
Tactic: rw [← zero_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
f g : (α → ℕ) → ℤ
hf : IsPoly f
hg : IsPoly g
⊢ IsPoly (f + g)
have rw : IsPoly (f - -g)
Tactic: rw [← sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x x_1 x_2 : Poly α
⊢ x + x_1 + x_2 = x + (x_1 + x_2)
have a : ∀ (x_3 : α → ℕ), Eq (α := ℤ) ((x + x_1 + x_2 : (a : α → ℕ) → ℤ) x_3 : ℤ) ((x + (x_1 + x_2) : (a : α → ℕ) → ℤ) x_3 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ 0 + x = x
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((0 + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((0 + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HAdd.hAdd (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: simp_rw [add_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((0 + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HAdd.hAdd (α := ℤ) (β := ℤ) (0 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: simp_rw [add_apply, zero_apply, zero_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ x + 0 = x
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((x + 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((x + 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HAdd.hAdd (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: simp_rw [add_apply, zero_apply, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
a :
  HAdd.hAdd (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ) =
    (x : (a : α → ℕ) → ℤ) x_1
⊢ Eq (α := ℤ) ((x + 0 : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a₁ : HAdd.hAdd (α := ℤ) (β := ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) (0 : ℤ) = (x : (a : α → ℕ) → ℤ) x_1
Tactic: simp_rw [add_apply, zero_apply, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
⊢ -x + x = 0
have a : ∀ (x_1 : α → ℕ), Eq (α := ℤ) ((-x + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Dioph (goal)
Goal:
α : Type u_1
β : Type u_2
x : Poly α
x_1 : α → ℕ
⊢ Eq (α := ℤ) ((-x + x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((0 : (a : α → ℕ) → ℤ) x_1 : ℤ)
have a : HAdd.hAdd (α := ℤ) (β := ℤ) ((-x : (a : α → ℕ) → ℤ) x_1 : ℤ) ((x : (a : α → ℕ) → ℤ) x_1 : ℤ) = (0 : (a : α → ℕ) → ℤ) x_1
Tactic: simp_rw [add_apply, neg_apply, neg_add_cancel, zero_apply]