no goals
ι : Type ?u.52291
ι' : Type ?u.52294
α : Type u_1
β : Type u_2
γ : Type ?u.52303
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ map (↑e) atTop = atTop
rw [← e.comap_atTop, map_comap_of_surjective e.surjective]