no goals
α : Type u_1
β : Type ?u.61301
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ infsep {x, y, z} = dist x y ⊓ dist x z ⊓ dist y z
simp only [infsep, einfsep_triple hxy hyz hxz, ENNReal.toReal_inf, edist_ne_top x y,
  edist_ne_top x z, edist_ne_top y z, dist_edist, Ne.def, inf_eq_top_iff, and_self_iff,
  not_false_iff]