no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.144553
ι : Sort x
f : Filter α
p : Prop
q : α → Prop
⊢ (∀ᶠ (x : α) in f, p → q x) ↔ p → ∀ᶠ (x : α) in f, q x
simp only [imp_iff_not_or, eventually_or_distrib_left]