α : Type u_1
β : Type ?u.55704
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = 0 ∨ Set.einfsep s = ⊤
α : Type u_1
β : Type ?u.55704
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ infsep s = 0
rw [infsep_zero.mpr]
case h
α : Type u_1
β : Type ?u.55704
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = ⊤
α : Type u_1
β : Type ?u.55704
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = 0 ∨ Set.einfsep s = ⊤
right
no goals
case h
α : Type u_1
β : Type ?u.55704
inst✝ : EDist α
x y : α
s : Set α
hs : Set.Subsingleton s
⊢ Set.einfsep s = ⊤
exact hs.einfsep