no goals
X : Type u_1
inst✝ : EMetricSpace X
s t : Set X
x✝ y : X
h : IsMetricSeparated s t
r : ENNReal
r0 : r ≠ 0
hr : ∀ (x : X), x ∈ s → ∀ (y : X), y ∈ t → r ≤ edist x y
x : X
hx1 : x ∈ s
hx2 : x ∈ t
⊢ r = 0
simpa using hr x hx1 x hx2