dsimp only [Filter.Frequently]
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (∃ᶠ (a : α) in f, p a) ↔ ∃ᶠ (a : α) in f, q a
α✝ : Type ?u.1842
α : Type u_1
f : Filter α
p q : α → Prop
h : ∀ᶠ (a : α) in f, p a ↔ q a
⊢ (¬∀ᶠ (x : α) in f, ¬p x) ↔ ¬∀ᶠ (x : α) in f, ¬q x