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