no goals
α : Type u
β : Type v
X : Type ?u.538230
ι : Type ?u.538233
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
r : ℝ
hr : 0 ≤ r
h : s ⊆ closedBall x r
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ r + r = 2 * r
simp [mul_two, mul_comm]