no goals
α : Type u_2
β : Type u_1
γ : Type ?u.59876
δ : Type ?u.59879
ι : Sort ?u.59882
f : Filter α
g : Filter β
s : Set (α × β)
la : Filter α
lb : Filter β
⊢ sᶜ ∈ Filter.coprod la lb ↔ (Prod.fst '' s)ᶜ ∈ la ∧ (Prod.snd '' s)ᶜ ∈ lb
simp only [Filter.coprod, mem_sup, compl_mem_comap]