-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_pow_sub_one_eq_prime_pow_of_ne_zero {k s : ℕ} (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1)))
    [hpri : Fact (p : ℕ).Prime] [hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L]
    (hirr : Irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (hs : s ≤ k) (hk : k ≠ 0) :
    norm K (ζ ^ (p : ℕ) ^ s - 1) = (p : K) ^ (p : ℕ) ^ s

Proof state:
case pos
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
⊢ (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Tactic:
have hp : p = 2 := by
  rw [← PNat.coe_inj, PNat.pow_coe, ← pow_one 2] at htwo
  replace htwo :=
    eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (succ_pos _) htwo
  rwa [show 2 = ((2 : ℕ+) : ℕ) by decide, PNat.coe_inj] at htwo

Result:
case pos
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
⊢ (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ↑p = 2
⊢ 2 = ↑2

Tactic:
decide

Result:
no goals

Proof state:
case pos.intro
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hpri : Fact (Nat.Prime ↑p)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hs : s = k
hζ : IsPrimitiveRoot ζ (2 ^ (k + 1))
hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)
hcycl : IsCyclotomicExtension {2 ^ (k + 1)} K L
k₁ : ℕ
hk₁ : k = k₁.succ
⊢ 2 ^ 2 ^ (k₁ + 1) = ↑2 ^ 2 ^ (k₁ + 1)

Tactic:
simp

Result:
no goals

Proof state:
case pos
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
⊢ (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Tactic:
replace hs : s = k := by
  rw [hp, ← PNat.coe_inj, PNat.pow_coe] at htwo
  nth_rw 2 [← pow_one 2] at htwo
  replace htwo := Nat.pow_right_injective rfl.le htwo
  rw [add_left_eq_self, Nat.sub_eq_zero_iff_le] at htwo
  exact le_antisymm hs htwo

Result:
case pos
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
hp : p = 2
hs : s = k
⊢ (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ↑p = 2
⊢ p = 2

Tactic:
rwa [show 2 = ((2 : ℕ+) : ℕ) by decide, PNat.coe_inj] at htwo

Result:
no goals

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : p ^ (k - s + 1) = 2
⊢ p = 2

Tactic:
rw [← PNat.coe_inj, PNat.pow_coe, ← pow_one 2] at htwo

Result:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ↑p ^ (k - s + 1) = ↑(2 ^ 1)
⊢ p = 2

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
hp : p = 2
htwo : k ≤ s
⊢ s = k

Tactic:
exact le_antisymm hs htwo

Result:
no goals

Proof state:
case neg
p : ℕ+
K : Type u
L : Type v
inst✝² : Field L
ζ : L
inst✝¹ : Field K
inst✝ : Algebra K L
k s : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
hs : s ≤ k
hk : k ≠ 0
htwo : ¬p ^ (k - s + 1) = 2
⊢ (Algebra.norm K) (ζ ^ ↑p ^ s - 1) = ↑↑p ^ ↑p ^ s

Tactic:
exact hζ.norm_pow_sub_one_of_prime_pow_ne_two hirr hs htwo

Result:
no goals