no goals
𝓕 : Type ?u.1001640
𝕜 : Type ?u.1001643
α : Type ?u.1001646
ι : Type ?u.1001649
κ : Type ?u.1001652
E : Type u_1
F : Type ?u.1001658
G : Type ?u.1001661
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
c : E
⊢ a * c ∈ ball (b * c) r ↔ a ∈ ball b r
simp only [mem_ball, dist_eq_norm_div, mul_div_mul_right_eq_div]