no goals
ι : Sort u_1
α : Type u_2
β : Type ?u.1140
l : Filter α
inst✝¹ : CountableInterFilter l
inst✝ : Countable ι
p : α → ι → Prop
⊢ (∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
simpa only [Filter.Eventually, setOf_forall] using
  @countable_iInter_mem _ _ l _ _ fun i => { x | p x i }