no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.142230
ι : Sort x
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, q x ↔ p x
simpa only [Iff.comm] using h