no goals
𝓕 : Type ?u.97056
𝕜 : Type ?u.97059
α : Type ?u.97062
ι : Type ?u.97065
κ : Type ?u.97068
E : Type u_1
F : Type ?u.97074
G : Type ?u.97077
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
h : b ∈ ball a r
⊢ ‖b / a‖ < r
rwa [← dist_eq_norm_div]