apply Set.ext
case heq
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ {x | x ∈ t → x ∈ s} = tᶜ ∪ s
case heq.h
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
⊢ ∀ (x : α), x ∈ {x | x ∈ t → x ∈ s} ↔ x ∈ tᶜ ∪ s