no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x : α
p : Filter ι
p' : Filter α
g : ι → α
u : Set (β × β)
x✝ : u ∈ 𝓤 β
⊢ ∀ᶠ (n : ι) in p, ∀ (x : α), x ∈ ∅ → (f x, F n x) ∈ u
simp