. exact superset_mem ha h
case mp
α : Type u_1
f : Filter α
s t a : Set α
ha : a ∈ f
b : Set α
hb : t ⊆ b
h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
⊢ {x | x ∈ t → x ∈ a ∩ b} ∈ f

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
⊢ a ⊆ {x | x ∈ t → x ∈ a ∩ b}