case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14614
inst✝ : EDist α
x y : α
s t : Set α
hs : einfsep s < ⊤
w✝¹ : α
hx : w✝¹ ∈ s
w✝ : α
hy : w✝ ∈ s
hxy : w✝¹ ≠ w✝
h✝ : edist w✝¹ w✝ < ⊤
⊢ Set.Nontrivial s
α : Type u_1
β : Type ?u.14614
inst✝ : EDist α
x y : α
s t : Set α
hs : einfsep s < ⊤
⊢ Set.Nontrivial s
rcases einfsep_lt_top.1 hs with ⟨_, hx, _, hy, hxy, _⟩
no goals
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.14614
inst✝ : EDist α
x y : α
s t : Set α
hs : einfsep s < ⊤
w✝¹ : α
hx : w✝¹ ∈ s
w✝ : α
hy : w✝ ∈ s
hxy : w✝¹ ≠ w✝
h✝ : edist w✝¹ w✝ < ⊤
⊢ Set.Nontrivial s
exact ⟨_, hx, _, hy, hxy⟩