no goals
𝓕 : Type ?u.95628
𝕜 : Type ?u.95631
α : Type ?u.95634
ι : Type ?u.95637
κ : Type ?u.95640
E : Type u_1
F : Type ?u.95646
G : Type ?u.95649
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r
rw [mem_closedBall', dist_eq_norm_div]