refine tendsto_prod_iff'.mpr ⟨lemma2, ?h⟩
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
case h
ι : Type u_1
α : Type u_2
β : Type u_3
a : α
s t : Set α
x u v : Set (α × α)
p : Filter ι
F : ι → α → β
f : α → β
inst✝ : UniformSpace β
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)
⊢ Tendsto (fun n => (f n.2, F n.1 n.2).2) (p ×ˢ 𝓟 s) (𝓝ᵘ (f '' s))