awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 - s).succ - 1) * p ^ s
Hex : k.succ - 1 = (k - s).succ - 1 + s
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s

Tactic:
mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this

Premises used: pow_ne_zero, mul_left_cancel₀, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 - s).succ - 1) * p ^ s
Hex : k.succ - 1 = (k - s).succ - 1 + s
⊢ Module.finrank (↥K⟮η⟯) L = p ^ s

Tactic:
exact mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this

Premises used: pow_ne_zero, mul_left_cancel₀, Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)

Tactic:
hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs fun h => ?_

Premises used: IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
refine : ∀ (h : p ^ (k - s + 1) = 2), False
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
refine hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs fun h => ?_

Premises used: IsPrimitiveRoot.norm_pow_sub_one_of_prime_pow_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ p ^ (k - s + 1) = HPow.hPow (α := ℕ) (β := ℕ) 2 1

Tactic:
rw [← pow_one 2] at h

Premises used: pow_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ 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
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 = 2
⊢ False

Tactic:
hodd h
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 = 2
⊢ False

Tactic:
exact hodd h
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
h : p ≠ 2
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑p : K) : K)

Tactic:
simpa using hζ.norm_pow_sub_one_of_prime_ne_two hirr k.zero_le h

Premises used: Nat.zero_le, IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ Irreducible (M := K[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) K)

Tactic:
simp [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ Irreducible (M := K[X]) (cyclotomic (p ^ HAdd.hAdd (α := ℕ) 0 1) K)

Tactic:
replace hirr : Irreducible (cyclotomic (p ^ (0 + 1)) K) := by simp [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
simp [hζ]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ IsPrimitiveRoot ζ (p ^ HAdd.hAdd (α := ℕ) 0 1)

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simp [hζ]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L

Tactic:
simp [hcyc]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L

Tactic:
haveI : IsCyclotomicExtension {p ^ (0 + 1)} K L := by simp [hcyc]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
this : IsCyclotomicExtension {p ^ HAdd.hAdd (α := ℕ) 0 1} K L
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) ((↑p : K) : K)

Tactic:
simpa using norm_sub_one_of_prime_ne_two hζ hirr h

Premises used: IsPrimitiveRoot.norm_sub_one_of_prime_ne_two
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ 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))
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ 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

Premises used: le_refl, Nat.le_succ, Nat.sub_self, Nat.succ_sub, pow_one, zero_lt_two, Nat.pow_div
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
simp : HSub.hSub (α := L) (-1) 1 = -2
⊢ HSub.hSub (α := L) (-1) 1 = (algebraMap K L : (a : K) → L) (-2)

Tactic:
simp only [map_neg, map_ofNat]

Premises used: map_ofNat, map_neg
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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 = -2

Tactic:
ring
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)

Tactic:
have H : (-1 : L) - (1 : L) = algebraMap K L (-2) := by
    simp only [map_neg, map_ofNat]
    ring
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
H : HSub.hSub (α := L) (-1) 1 = (algebraMap K L : (a : K) → L) (-2)
⊢ Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)

Tactic:
simp [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
H : HSub.hSub (α := L) (-1) 1 = (algebraMap K L : (a : K) → L) (-2)
⊢ Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 (k + 1)) K)

Tactic:
replace hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K) := by simp [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
rw :
  HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1) =
    HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ HPow.hPow (α := ℕ) 2 k - 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]

Premises used: Nat.totient_prime_pow, Nat.zero_lt_succ, IsCyclotomicExtension.finrank, Nat.prime_two, tsub_zero, Algebra.norm_algebraMap, IsPrimitiveRoot.eq_neg_one_of_two_right, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k * HSub.hSub (α := ℕ) 2 1) =
    HPow.hPow (α := K) (-2) (HPow.hPow (α := ℕ) 2 k)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 1 < HPow.hPow (α := ℕ) 2 k

Tactic:
Nat.pow_lt_pow_right one_lt_two (lt_of_lt_of_le one_lt_two hk)

Premises used: one_lt_two, Nat.pow_lt_pow_right, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 1 < HPow.hPow (α := ℕ) 2 k

Tactic:
exact Nat.pow_lt_pow_right one_lt_two (lt_of_lt_of_le one_lt_two hk)

Premises used: one_lt_two, Nat.pow_lt_pow_right, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
⊢ 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)
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
this : 2 < HPow.hPow (α := ℕ) 2 k
⊢ Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)

Tactic:
simp [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
this : 2 < HPow.hPow (α := ℕ) 2 k
⊢ Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)

Tactic:
replace hirr : Irreducible (cyclotomic (2 ^ k) K) := by simp [hirr]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
this : 2 < HPow.hPow (α := ℕ) 2 k
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 k)

Tactic:
simp [hζ]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
this : 2 < HPow.hPow (α := ℕ) 2 k
hirr : Irreducible (M := K[X]) (cyclotomic (HPow.hPow (α := ℕ) 2 k) K)
⊢ IsPrimitiveRoot ζ (HPow.hPow (α := ℕ) 2 k)

Tactic:
replace hζ : IsPrimitiveRoot ζ (2 ^ k) := by simp [hζ]
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
obtain : ∀ (k₁ : ℕ) (hk₁ : k = k₁.succ), Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) (2 : K)
⊢ 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

Premises used: Ne.symm, Nat.exists_eq_succ_of_ne_zero, zero_lt_two, lt_of_lt_of_le, LT.lt.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ Eq.{u + 1} (α := K) ((Algebra.norm K : (a : L) → K) (ζ - 1) : K) (2 : K)

Tactic:
simpa [hk₁] using sub_one_norm_eq_eval_cyclotomic hζ this hirr

Premises used: IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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)
neg :
  ∀ (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)

Tactic:
by_cases htwo : p ^ (k - s + 1) = 2

Premises used: HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ p = 2

Tactic:
obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo

Premises used: Nat.prime_two, Iff.mp, Nat.Prime.pow_eq_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ k - s + 1 = 1

Tactic:
obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo

Premises used: Nat.prime_two, Iff.mp, Nat.Prime.pow_eq_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ k - s = 0

Tactic:
simp only [add_eq_right] at hks

Premises used: add_eq_right
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
⊢ s = k

Tactic:
replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
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)
⊢ (Algebra.norm K : (a : L) → K) (ζ ^ p ^ s - 1) = HPow.hPow (α := K) (↑p : K) (p ^ s)

Tactic:
simp only [hp, hs] at hζ hirr hcycl ⊢
-- Module: Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
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
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)
⊢ (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

Premises used: Nat.exists_eq_succ_of_ne_zero