. intros h
  exact h _ (mem_principal_self s)
case mp
α : Type u_1
s : Set α
f : Filter α
⊢ f ≤ 𝓟 s → s ∈ f

case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s
case mpr
α : Type u_1
s : Set α
f : Filter α
⊢ s ∈ f → f ≤ 𝓟 s