have heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s ∈ f ⊓ 𝓟 t
case heq
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
⊢ s = (tᶜ ∪ s) ∩ (t ∪ s)

case mpr
α : Type u_1
f : Filter α
s t : Set α
h : tᶜ ∪ s ∈ f
heq : s = (tᶜ ∪ s) ∩ (t ∪ s)
⊢ s ∈ f ⊓ 𝓟 t