ι : Type ?u.282150
ι' : Type ?u.282153
α : Type u_1
β : Type ?u.282159
γ : Type ?u.282162
inst✝ : SemilatticeSup α
⊢ Tendsto (fun a => (a, a)) atTop (atTop ×ˢ atTop)
ι : Type ?u.282150
ι' : Type ?u.282153
α : Type u_1
β : Type ?u.282159
γ : Type ?u.282162
inst✝ : SemilatticeSup α
⊢ Tendsto (fun a => (a, a)) atTop atTop
rw [← prod_atTop_atTop_eq]
no goals
ι : Type ?u.282150
ι' : Type ?u.282153
α : Type u_1
β : Type ?u.282159
γ : Type ?u.282162
inst✝ : SemilatticeSup α
⊢ Tendsto (fun a => (a, a)) atTop (atTop ×ˢ atTop)
exact tendsto_id.prod_mk tendsto_id