no goals
𝕜 : Type ?u.1761797
E : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
⊢ r • closedBall 0 1 = closedBall 0 r
rw [smul_closedUnitBall, Real.norm_of_nonneg hr]