case intro
ι : Sort ?u.57852
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
y : α
hy : y ∈ s
⊢ infEdist x s ≠ ⊤
ι : Sort ?u.57852
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y : α
Φ : α → β
h : Set.Nonempty s
⊢ infEdist x s ≠ ⊤
rcases h with ⟨y, hy⟩
no goals
case intro
ι : Sort ?u.57852
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s t u : Set α
x y✝ : α
Φ : α → β
y : α
hy : y ∈ s
⊢ infEdist x s ≠ ⊤
exact ne_top_of_le_ne_top (edist_ne_top _ _) (infEdist_le_edist_of_mem hy)