no goals
𝕜 : Type ?u.1476288
E : Type u_1
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
x y z : E
δ ε : ℝ
inst✝ : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)
rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
  Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]