no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.142957
ι✝ : Sort x
ι : Type u_1
I : Set ι
hI : Set.Finite I
l : Filter α
p : ι → α → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), i ∈ I → p i x) ↔ ∀ (i : ι), i ∈ I → ∀ᶠ (x : α) in l, p i x
simpa only [Filter.Eventually, setOf_forall] using biInter_mem hI