rw [mul_comm, zpow_mul, zpow_ofNat]
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ hζ.unit' ^ (2 * ↑k) = (hζ.unit' ^ k) ^ 2
case h.e'_4.h.e'_6.h.e'_5.h.e'_3
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ : ℤ
hpodd : p ≠ 2
hp : (↑p).Prime
x y i : ℤ
u : (𝓞 K)ˣ
α : 𝓞 K
h : ↑x + ↑y * ↑(hζ.unit' ^ i) = ↑u * α ^ ↑p
k : ℕ
hk : ↑x + ↑y * ↑(hζ.unit' ^ i) - ↑((hζ.unit' ^ k) ^ 2) * (↑x + ↑y * ↑(hζ.unit' ^ (-i))) ∈ Ideal.span {↑↑p}
⊢ (hζ.unit' ^ ↑k) ^ 2 = (hζ.unit' ^ k) ^ 2