no goals
𝓕 : Type ?u.105197
𝕜 : Type ?u.105200
α : Type ?u.105203
ι : Type ?u.105206
κ : Type ?u.105209
E : Type u_1
F : Type ?u.105215
G : Type ?u.105218
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
hr : r ≠ 0
x : ↑(sphere 1 r)
⊢ ‖↑x‖ ≠ 0
rwa [norm_eq_of_mem_sphere' x]