no goals
α : Type u
β : Type v
X : Type ?u.37806
ι : Type ?u.37809
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ closedBall x ε \ sphere x ε = ball x ε
rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]