-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_pow_sub_one_two {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1)))
    [IsCyclotomicExtension {(2 : ℕ+) ^ (k + 1)} K L]
    (hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)) :
    norm K (ζ ^ 2 ^ k - 1) = (-2 : K) ^ 2 ^ k

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ (k + 1) / 2 ^ k)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
rw [Nat.pow_div (le_succ k) zero_lt_two, Nat.succ_sub (le_refl k), Nat.sub_self, pow_one] at this

Result:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ -1 - 1 = -2

Tactic:
ring

Result:
no goals

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
have H : (-1 : L) - (1 : L) = algebraMap K L (-2) := by
  simp only [map_neg, map_ofNat]
  ring

Result:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
replace hirr : Irreducible (cyclotomic ((2 : ℕ+) ^ (k + 1) : ℕ+) K) := by simp [hirr]

Result:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
hirr : Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
hirr : Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
rw [this.eq_neg_one_of_two_right, H, Algebra.norm_algebraMap,
  IsCyclotomicExtension.finrank L hirr, pow_coe, show ((2 : ℕ+) : ℕ) = 2 from rfl,
    totient_prime_pow Nat.prime_two (zero_lt_succ k), succ_sub_succ_eq_sub, tsub_zero]

Result:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
hirr : Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)
⊢ (-2) ^ (2 ^ k * (2 - 1)) = (-2) ^ 2 ^ k

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Tactic:
have := hζ.pow_of_dvd (fun h => two_ne_zero (pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k))

Result:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) (2 ^ (k + 1) / 2 ^ k)
⊢ (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ -1 - 1 = (algebraMap K L) (-2)

Tactic:
simp only [map_neg, map_ofNat]

Result:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
⊢ -1 - 1 = -2

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
⊢ Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)

Tactic:
simp [hirr]

Result:
no goals

Proof state:
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
inst✝ : IsCyclotomicExtension {2 ^ (k + 1)} K L
this : IsPrimitiveRoot (ζ ^ 2 ^ k) 2
H : -1 - 1 = (algebraMap K L) (-2)
hirr : Irreducible (cyclotomic (↑(2 ^ (k + 1))) K)
⊢ (-2) ^ (2 ^ k * (2 - 1)) = (-2) ^ 2 ^ k

Tactic:
simp

Result:
no goals