no goals
α : Type u
β : Type v
γ : Type ?u.12644
f g : Ultrafilter α
s t : Set α
p q : α → Prop
⊢ (∀ᶠ (x : α) in ↑f, p x → q x) ↔ (∀ᶠ (x : α) in ↑f, p x) → ∀ᶠ (x : α) in ↑f, q x
simp only [imp_iff_not_or, eventually_or, eventually_not]