no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.288409
ι : Sort x
F : Filter α
s : Set α
⊢ F ⊓ 𝓟 s = ⊥ ↔ comap Subtype.val F = ⊥
rw [principal_eq_map_coe_top s, ← Filter.push_pull', inf_top_eq, map_eq_bot_iff]