no goals
𝓕 : Type ?u.93611
𝕜 : Type ?u.93614
α : Type ?u.93617
ι : Type ?u.93620
κ : Type ?u.93623
E : Type u_1
F : Type ?u.93629
G : Type ?u.93632
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ a ∈ ball 1 r ↔ ‖a‖ < r
rw [mem_ball, dist_one_right]