no goals
𝕜 : Type ?u.441668
𝕜' : Type ?u.441671
E : Type u_1
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedField 𝕜'
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜' E
r✝ : ℝ
inst✝ : CharZero 𝕜
r : ℝ
hr : r ≠ 0
x : ↑(sphere 0 r)
h : x = -x
⊢ ↑x = -↑x
conv_lhs => rw [h]