use b, ↑u * ((hζ.unit' - 1 : 𝓞 K) * k ^ (p : ℕ)) - r
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
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p
case h
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
u : (𝓞 K)ˣ
hr : ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p)) = a ^ ↑p - ↑b ^ ↑p + ↑↑p * r
hu : ↑↑p * ↑u = (↑hζ.unit' - 1) ^ (↑p - 1)
⊢ a ^ ↑p - ↑b ^ ↑p = ↑↑p * (↑u * ((↑hζ.unit' - 1) * k ^ ↑p) - r)