. intros hs
  rw [mem_inf_def] at hs
  have ⟨a, ha, b, hb, hsab⟩ := hs
  clear hs
  rw [hsab]; clear hsab
  rw [mem_principal_def] at hb
  suffices h : a ⊆ {x | x ∈ t → x ∈ a ∩ b}
  . exact superset_mem ha h
  intros x hxa hxt
  exact ⟨hxa, hb hxt⟩
case mp
α : Type u_1
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t → {x | x ∈ t → x ∈ s} ∈ f

case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t