no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.117799
ι : Sort x
f✝ g : Filter α
s✝ t✝ : Set α
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f
simp only [← le_principal_iff, (isCompl_principal s).le_left_iff, disjoint_assoc, inf_principal,
  ← (isCompl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]