obtain ⟨n, hn0, hn⟩ := h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
hpo : Odd ↑p
x : K
h : ∃ n, ∃ (_ : 0 < n), x ^ n = 1
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
case 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
⊢ ∃ m k, x = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m