no goals
α : Type u
β : Type v
X : Type ?u.198627
ι : Type ?u.198630
inst✝ : PseudoMetricSpace α
x r y : ℝ
⊢ y ∈ ball x r ↔ y ∈ Ioo (x - r) (x + r)
rw [mem_ball, dist_comm, Real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add',
  sub_lt_comm]