no goals
𝕜 : Type ?u.232934
E : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
x✝ y z : E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
x : E
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]