no goals
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
⊢ Tendsto (fun p => (u p.fst, u p.snd)) (atTop ×ˢ atTop) (𝓤 α) ↔ Tendsto (Prod.map u u) atTop (𝓤 α)
simp only [prod_atTop_atTop_eq, Prod.map_def]