no goals
ι : Sort ?u.68670
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x✝ y✝ : α
Φ : α → β
h : IsCompact s
hne : Set.Nonempty s
x y : α
hys : y ∈ s
hy : infEdist x s = edist x y
⊢ infDist x s = dist x y
rw [infDist, dist_edist, hy]