rw [heq] at h
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : {x | x ∈ t → x ∈ s} ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
⊢ s ∈ f ⊓ 𝓟 t