no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s s' : Set α
x✝ : α
p : Filter ι
p' : Filter α
g : ι → α
inst✝ : TopologicalSpace α
hs : IsOpen s
x : α
hx : x ∈ s
⊢ Tendsto (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝[s] x) (𝓤 β) ↔
    Tendsto (fun y => (f y.snd, F y.fst y.snd)) (p ×ˢ 𝓝 x) (𝓤 β)
rw [hs.nhdsWithin_eq hx]