α : Type u_1
β : Type ?u.15427
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Subsingleton s
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
α : Type u_1
β : Type ?u.15427
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = ⊤
rw [einfsep_top]
no goals
α : Type u_1
β : Type ?u.15427
inst✝ : EDist α
x y : α
s t : Set α
hs : Set.Subsingleton s
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → edist x y = ⊤
exact fun _ hx _ hy hxy => (hxy <| hs hx hy).elim