no goals
τ : Type u_2
α : Type u_4
β : Type u_3
ι : Type ?u.26859
inst✝ : TopologicalSpace β
f✝ : Filter τ
ϕ✝ : τ → α → β
s s₁ s₂ : Set α
α' : Type u_1
ϕ : τ → α' → β
f : Filter τ
g : α → α'
⊢ ω f ϕ (g '' s) = ω f (fun t x => ϕ t (g x)) s
simp only [omegaLimit, image2_image_right]