no goals
ι : Type ?u.279380
ι' : Type ?u.279383
α : Type ?u.279386
β : Type ?u.279389
γ : Type ?u.279392
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
inst✝¹ : Preorder β₁
inst✝ : Preorder β₂
u₁ : β₁ → α₁
u₂ : β₂ → α₂
⊢ map u₁ atTop ×ˢ map u₂ atTop = map (Prod.map u₁ u₂) atTop
rw [prod_map_map_eq, prod_atTop_atTop_eq, Prod.map_def]