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