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