no goals
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : SemilatticeSup β
u : β → α
h : CauchySeq u
⊢ Tendsto (Prod.map u u) atTop (𝓤 α)
simpa only [Tendsto, prod_map_map_eq', prod_atTop_atTop_eq] using h.right