no goals
α : Type u_1
β : Type ?u.34662
inst✝¹ : EDist α
x y : α
s✝ t : Set α
inst✝ : DecidableEq α
s : Finset α
⊢ einfsep ↑s = Finset.inf (Finset.offDiag s) (uncurry edist)
simp_rw [einfsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]