no goals
ι : Type ?u.49076
ι' : Type ?u.49079
α : Type u_1
β : Type u_2
γ : Type ?u.49088
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
⊢ comap (↑e) atTop = atTop
simp [atTop, ← e.surjective.iInf_comp]