no goals
𝕜 : Type ?u.1204873
E : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_comm δ]