no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.226876
ι : Sort x
f : α → β
l : Filter β
p : α → Prop
s : Set α
⊢ s ∈ comap f l ↔ (f '' sᶜ)ᶜ ∈ l
simp only [mem_comap', compl_def, mem_image, mem_setOf_eq, not_exists, not_and', not_not]