no goals
𝓕 : Type ?u.742261
𝕜 : Type ?u.742264
α : Type ?u.742267
ι : Type ?u.742270
κ : Type ?u.742273
E : Type u_1
F : Type ?u.742279
G : Type ?u.742282
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ a * b ∈ closedBall a r ↔ ‖b‖ ≤ r
rw [mem_closedBall_iff_norm'', mul_div_cancel''']