case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10402
δ : Type ?u.10405
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
t : Set ?m.10680
ht : IsCompact t
hts : ?m.10705ᶜ ⊆ t
⊢ IsCompact (↑f ⁻¹' s)
α : Type u_2
β : Type u_1
γ : Type ?u.10402
δ : Type ?u.10405
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ IsCompact (↑f ⁻¹' s)
obtain ⟨t, ht, hts⟩ :=
  mem_cocompact'.mp
    (by
      simpa only [preimage_image_preimage, preimage_compl] using
        mem_map.mp
          (cocompact_tendsto f <|
            mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))
no goals
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10402
δ : Type ?u.10405
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
t : Set ?m.10680
ht : IsCompact t
hts : ?m.10705ᶜ ⊆ t
⊢ IsCompact (↑f ⁻¹' s)
exact
  isCompact_of_isClosed_subset ht (hs.isClosed.preimage <| map_continuous f) (by simpa using hts)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.10402
δ : Type ?u.10405
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ ?m.10705 ∈ cocompact α
simpa only [preimage_image_preimage, preimage_compl] using
  mem_map.mp
    (cocompact_tendsto f <|
      mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.10402
δ : Type ?u.10405
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
t : Set α
ht : IsCompact t
hts : (↑f ⁻¹' s)ᶜᶜ ⊆ t
⊢ ↑f ⁻¹' s ⊆ t
simpa using hts