no goals
ι : Type u_2
α✝ : Type ?u.3999
β : Type ?u.4002
l : Filter α✝
α : ι → Type u_1
inst✝ : Finite ι
s : Set ((i : ι) → α i)
⊢ (sᶜ ∈ Filter.coprodᵢ fun i => cofinite) ↔ sᶜ ∈ cofinite
simp only [compl_mem_coprodᵢ, mem_cofinite, compl_compl, forall_finite_image_eval_iff]