simp [u, and_assoc]
α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
s t : Finset α
a : α
h : ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
u : Finset α := filter (fun w => ∀ a ∈ s, a ∉ t → a < w) (t \ s)
w : α
⊢ w ∈ u ↔ w ∈ t ∧ w ∉ s ∧ ∀ a ∈ s, a ∉ t → a < w
no goals