Theorem: Filter.frequently_congr (Sion/ForMathlib/Misc.lean)

State before:
α : Type u_1
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
Tactic:
simpa only [Iff.comm] using h
State after:
no goals