no goals
α : Type u
β : Type v
X : Type ?u.37673
ι : Type ?u.37676
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ sphere x ε ∪ ball x ε = closedBall x ε
rw [union_comm, ball_union_sphere]