rw [pow_mul, hζ.unit'_pow, one_pow]
case h.e'_3.h.e'_5
p : ℕ+
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
n : ℕ
h✝ : n ≠ 0
r : ℕ
hr : ↑p = 2 * r + 1
he : 2 * (r + 1) * n = ↑p * n + n
⊢ hζ.unit' ^ (↑p * n) = 1
no goals