rw [← eq, hmk]
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
n : ℕ
hn0 : 0 < n
hn : x ^ n = 1
hx : IsIntegral ℤ x
hxu : ⟨x, hx⟩ ^ n = 1
m : ℕ
k : ℕ+
hmk : ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
eq : ↑⟨x, hx⟩ = x
⊢ x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
no goals