no goals
E : Type u_1
inst✝ : SeminormedCommGroup E
ε δ : ℝ
s t : Set E
x y : E
⊢ {x} * ball y δ = ball (x * y) δ
simp only [preimage_mul_ball, image_mul_left, singleton_mul, div_inv_eq_mul, mul_comm y x]