no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.299000
ι : Sort x
f : Filter α
g : α → Filter β
s✝ s : Set β
⊢ (s ∈ bind f fun x => g x ⊓ 𝓟 s✝) ↔ s ∈ bind f g ⊓ 𝓟 s✝
simp only [mem_bind, mem_inf_principal]