no goals
α : Type u_1
β : Type ?u.76474
inst✝¹ : PseudoMetricSpace α
x y z : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
hs : Finset.Nonempty (Finset.offDiag s)
⊢ infsep ↑s = Finset.inf' (Finset.offDiag s) hs (uncurry dist)
rw [Finset.coe_infsep, dif_pos hs]