no goals
α : Type u
β : Type v
X : Type ?u.528785
ι : Type ?u.528788
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
hs : Set.Subsingleton s
⊢ diam s = 0
simp only [diam, EMetric.diam_subsingleton hs, ENNReal.zero_toReal]