no goals
α : Type u_1
β : Type ?u.58192
inst✝ : PseudoMetricSpace α
x y z : α
s t : Set α
d : ℝ
hs : Set.Nontrivial s
⊢ d ≤ infsep s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → d ≤ dist x y
simp_rw [infsep, ← ENNReal.ofReal_le_iff_le_toReal hs.einfsep_ne_top, le_einfsep_iff, edist_dist,
  ENNReal.ofReal_le_ofReal_iff dist_nonneg]