no goals
α : Type u
β : Type v
X : Type ?u.200414
ι : Type ?u.200417
inst✝ : PseudoMetricSpace α
x y : ℝ
⊢ Ioo x y = ball ((x + y) / 2) ((y - x) / 2)
rw [Real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, add_sub_cancel', add_self_div_two,
  ← add_div, add_assoc, add_sub_cancel'_right, add_self_div_two]