rw [eq_comm, ← sub_eq_zero, ← hr]
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 2
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
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
p : ℕ
hpri : p.Prime
hp : p ≠ 2
x : 𝓞 K
hx : IsUnit (1 + p • x)
H : (Algebra.norm ℤ) (1 + p • x) = 1 ∨ (Algebra.norm ℤ) (1 + p • x) = -1
e : (Algebra.norm ℤ) (1 + p • x) = -1
r : ℤ
hr : 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1 = 0
⊢ 2 - ↑p * (-(Algebra.trace ℤ (𝓞 K)) x - r * ↑p) = 1 + (Algebra.trace ℤ (𝓞 K)) x * ↑p + r * ↑p ^ 2 - -1