no goals
𝓕 : Type ?u.741114
𝕜 : Type ?u.741117
α : Type ?u.741120
ι : Type ?u.741123
κ : Type ?u.741126
E : Type u_1
F : Type ?u.741132
G : Type ?u.741135
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ a * b ∈ ball a r ↔ ‖b‖ < r
rw [mem_ball_iff_norm'', mul_div_cancel''']