[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f g : CocompactMap α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
g : CocompactMap α β
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
cocompact_tendsto'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (cocompact β)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ } =
    (fun f => f.toFun) g
⊢ { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ } = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
cocompact_tendsto'✝¹ : Tendsto (ContinuousMap.mk toFun✝¹).toFun (cocompact α) (cocompact β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
cocompact_tendsto'✝ : Tendsto (ContinuousMap.mk toFun✝).toFun (cocompact α) (cocompact β)
h :
  (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝¹, cocompact_tendsto' := cocompact_tendsto'✝¹ } =
    (fun f => f.toFun) { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ }
⊢ { toContinuousMap := ContinuousMap.mk toFun✝¹, cocompact_tendsto' := cocompact_tendsto'✝¹ } =
    { toContinuousMap := ContinuousMap.mk toFun✝, cocompact_tendsto' := cocompact_tendsto'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Continuous f'
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Continuous ↑f
[PROOFSTEP]
exact f.continuous_toFun
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Tendsto (ContinuousMap.mk f').toFun (cocompact α) (cocompact β)
[PROOFSTEP]
simp_rw [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = ↑f
⊢ Tendsto (↑f) (cocompact α) (cocompact β)
[PROOFSTEP]
exact f.cocompact_tendsto'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)
s : Set β
hs : s ∈ cocompact β
t : Set β
ht : IsCompact t
hts : tᶜ ⊆ s
⊢ (f ⁻¹' t)ᶜ ⊆ f ⁻¹' s
[PROOFSTEP]
simpa using preimage_mono hts
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ IsCompact (↑f ⁻¹' s)
[PROOFSTEP]
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 _)⟩))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : TopologicalSpace δ
inst✝ : T2Space β
f : CocompactMap α β
s : Set β
hs : IsCompact s
⊢ ?m.10429 ∈ cocompact ?m.10404
[PROOFSTEP]
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 _)⟩)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
⊢ IsCompact (↑f ⁻¹' s)
[PROOFSTEP]
exact isCompact_of_isClosed_subset ht (hs.isClosed.preimage <| map_continuous f) (by simpa using hts)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
simpa using hts
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
⊢ Tendsto (ContinuousMap.mk ↑f).toFun (cocompact α) (cocompact β)
[PROOFSTEP]
refine' CocompactMap.tendsto_of_forall_preimage fun K hK => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ IsCompact ((ContinuousMap.mk ↑f).toFun ⁻¹' K)
[PROOFSTEP]
erw [K.preimage_equiv_eq_image_symm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ IsCompact (↑f.symm '' K)
[PROOFSTEP]
exact hK.image f.symm.continuous
