-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- The preimage of a compact set by a proper map is again compact. See also
`isProperMap_iff_isCompact_preimage` which proves that this property completely characterizes
proper map when the codomain is compactly generated and Hausdorff. -/
lemma IsProperMap.isCompact_preimage (h : IsProperMap f) {K : Set Y} (hK : IsCompact K) :
    IsCompact (f ⁻¹' K)

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
x : X
hx : ↑𝒰 ≤ 𝓝 x
hyK : f x ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 (f x)
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Tactic:
exact ⟨x, hyK, hx⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Tactic:
rcases hK.ultrafilter_le_nhds _ h𝒰 with ⟨y, hyK, hy⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
y : Y
hyK : y ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ ∀ (f_1 : Ultrafilter X), ↑f_1 ≤ 𝓟 (f ⁻¹' K) → ∃ x ∈ f ⁻¹' K, ↑f_1 ≤ 𝓝 x

Tactic:
intro 𝒰 h𝒰

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑𝒰 ≤ 𝓟 (f ⁻¹' K)
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Tactic:
rw [← comap_principal, ← map_le_iff_le_comap, ← Ultrafilter.coe_map] at h𝒰

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
⊢ ∀ (f_1 : Ultrafilter X), ↑f_1 ≤ 𝓟 (f ⁻¹' K) → ∃ x ∈ f ⁻¹' K, ↑f_1 ≤ 𝓝 x

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
y : Y
hyK : y ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 y
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x

Tactic:
rcases h.ultrafilter_le_nhds_of_tendsto hy with ⟨x, rfl, hx⟩

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
h : IsProperMap f
K : Set Y
hK : IsCompact K
𝒰 : Ultrafilter X
h𝒰 : ↑(Ultrafilter.map f 𝒰) ≤ 𝓟 K
x : X
hx : ↑𝒰 ≤ 𝓝 x
hyK : f x ∈ K
hy : ↑(Ultrafilter.map f 𝒰) ≤ 𝓝 (f x)
⊢ ∃ x ∈ f ⁻¹' K, ↑𝒰 ≤ 𝓝 x