. intros h
  have heq : {x | x ∈ t → x ∈ s} = tᶜ ∪ s
  . apply Set.ext; intros x
    rw [Set.mem_iff, Set.mem_union, Set.mem_compl_iff, imp_iff_not_or]
  rw [heq] at h; clear heq
  have heq : s = (tᶜ ∪ s) ∩ (t ∪ s) 
  . rw [← Set.union_distrib_right, Set.compl_inter_self, Set.empty_union]
  rw [heq]; clear heq
  refine inter_mem_inf h ?_
  rw [mem_principal_def]
  exact Set.subset_union_left _ _
case mpr
α : Type u_1
f : Filter α
s t : Set α
⊢ {x | x ∈ t → x ∈ s} ∈ f → s ∈ f ⊓ 𝓟 t
no goals