exact hat $ (hw $ hwa.lt_of_ne $ ne_of_mem_of_not_mem hwt hat).1 has
case refine_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a✝ w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
a : α
has : a ∈ s
hat : a ∉ t
hwa : w ≤ a
⊢ False
no goals