obtain ⟨ζ, hζ⟩ := IsCyclotomicExtension.exists_prim_root ℚ (B := K) (Set.mem_singleton p)
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
hp : p ≠ 2
a : 𝓞 K
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
case intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ✝ : K
hζ✝ : IsPrimitiveRoot ζ✝ ↑p
hp : p ≠ 2
a : 𝓞 K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p