no goals
𝕜 : Type ?u.1779223
E : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
⊢ x +ᵥ r • ball 0 1 = ball x r
rw [smul_unitBall_of_pos hr, vadd_ball_zero]