no goals
ι : Type ?u.3352
α : Type u_1
β : Type u_2
l : Filter α
s : Set (α × β)
⊢ sᶜ ∈ Filter.coprod cofinite cofinite ↔ sᶜ ∈ cofinite
simp only [compl_mem_coprod, mem_cofinite, compl_compl, finite_image_fst_and_snd_iff]