rw [(Nat.Prime.odd_of_ne_two hpri.out (PNat.coe_injective.ne hp)).neg_pow, ← sub_eq_add_neg, e,
  mul_pow, ← sub_eq_add_neg] at hr
case intro.intro.intro.intro.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 : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (a + -↑b) ^ ↑p = a ^ ↑p + (-↑b) ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
case intro.intro.intro.intro.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 : ℤ
k : 𝓞 K
e : a - ↑b = (↑hζ.unit' - 1) * k
r : 𝓞 K
hr : (↑hζ.unit' - 1) ^ ↑p * k ^ ↑p = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p