obtain ⟨i, _, Hi⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one isPrimRoot hxp'' p.prop
case intro.intro.inl
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
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hxp' : ⟨x, hx⟩ ^ (2 * ↑p) = 1
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m
case intro.intro.inl.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
l : ℕ
hl : l ∈ n.divisors
hhl : (cyclotomic l ↥(integralClosure ℤ K)).IsRoot ⟨x, hx⟩
hlp : l ∣ 2 * ↑p
isPrimRoot : IsPrimitiveRoot ↑hζ.unit' ↑p
hxl : ⟨x, hx⟩ ^ l = 1
hxp' : ⟨x, hx⟩ ^ (2 * ↑p) = 1
hxp'' : ⟨x, hx⟩ ^ ↑p = 1
i : ℕ
left✝ : i < ↑p
Hi : ↑hζ.unit' ^ i = ⟨x, hx⟩
⊢ ∃ m k, ↑⟨x, hx⟩ = (-1) ^ ↑k * (algebraMap (𝓞 K) K) ↑hζ.unit' ^ m