no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.190339
ι : Sort x
s t : Set α
l : Filter α
⊢ s ∩ t =ᶠ[l] s ↔ ∀ᶠ (x : α) in l, x ∈ s → x ∈ t
simp only [eventuallyEq_set, mem_inter_iff, and_iff_left_iff_imp]