no goals
ι : Sort ?u.60248
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
r : ℝ
hs : Set.Nonempty s
⊢ infDist x s < r ↔ ∃ y, y ∈ s ∧ dist x y < r
simp_rw [infDist, ← ENNReal.lt_ofReal_iff_toReal_lt (infEdist_ne_top hs), infEdist_lt_iff,
  ENNReal.lt_ofReal_iff_toReal_lt (edist_ne_top _ _), ← dist_edist]