no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.226477
ι : Sort x
f : α → β
l : Filter β
p : α → Prop
s : Set α
⊢ (∃ᶠ (a : α) in comap f l, p a) ↔ ∃ᶠ (b : β) in l, ∃ a, f a = b ∧ p a
simp only [Filter.Frequently, eventually_comap, not_exists, not_and]