no goals
α : Type u_1
β : Type u_2
γ : Type ?u.62010
δ : Type ?u.62013
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
⊢ map (↑h) (cocompact α) = cocompact β
rw [← h.comap_cocompact, map_comap_of_surjective h.surjective]