no goals
α : Type u
β : Type v
X : Type ?u.296438
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
⊢ diam {x, y} = edist x y
simp only [iSup_singleton, diam_insert, diam_singleton, ENNReal.max_zero_right]