no goals
τ : Type u_2
α : Type u_3
β : Type u_1
ι : Type ?u.30321
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s ↔ ∀ (n : Set β), n ∈ 𝓝 y → ∃ᶠ (t : τ) in f, Set.Nonempty (ϕ t '' s ∩ n)
simp_rw [mem_omegaLimit_iff_frequently, image_inter_nonempty_iff]