case h
α : Type u
β : Type v
X : Type ?u.199537
ι : Type ?u.199540
inst✝ : PseudoMetricSpace α
x r y : ℝ
⊢ y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)
α : Type u
β : Type v
X : Type ?u.199537
ι : Type ?u.199540
inst✝ : PseudoMetricSpace α
x r : ℝ
⊢ closedBall x r = Icc (x - r) (x + r)
ext y
no goals
case h
α : Type u
β : Type v
X : Type ?u.199537
ι : Type ?u.199540
inst✝ : PseudoMetricSpace α
x r y : ℝ
⊢ y ∈ closedBall x r ↔ y ∈ Icc (x - r) (x + r)
rw [mem_closedBall, dist_comm, Real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add',
  sub_le_comm]