intros x hxa hxt
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}
case h
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
x : α
hxa : x ∈ a
hxt : x ∈ t
⊢ x ∈ a ∩ b