-- Mathlib/Topology/Maps/Proper/Basic.lean
theorem isProperMap_iff_isClosedMap_and_compact_fibers :
    IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ y, IsCompact (f ⁻¹' {y})

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
exact ⟨H.continuous, H.isClosedMap, fun y ↦ H.isCompact_preimage isCompact_singleton⟩

Result:
no goals

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x ℱ

Tactic:
rw [← clusterPt_lift'_closure_iff]

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (ℱ.lift' closure)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
constructor <;> intro H

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_clusterPt]

Result:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x (ℱ.lift' closure)

Tactic:
exact hx.mono inf_le_left

Result:
no goals

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
rw [H.2.1.mapClusterPt_iff_lift'_closure H.1] at hy

Result:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ Continuous f ∧ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
refine ⟨H.1, fun ℱ y hy ↦ ?_⟩

Result:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : MapClusterPt y ℱ f
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Proof state:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
refine ⟨x, hxy, ?_⟩

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ClusterPt x ℱ

Proof state:
case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ

Tactic:
rcases H.2.2 y (f := Filter.lift' ℱ closure ⊓ 𝓟 (f ⁻¹' {y})) inf_le_right with ⟨x, hxy, hx⟩

Result:
case mpr.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
ℱ : Filter X
y : Y
hy : (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y})).NeBot
x : X
hxy : x ∈ f ⁻¹' {y}
hx : ClusterPt x (ℱ.lift' closure ⊓ 𝓟 (f ⁻¹' {y}))
⊢ ∃ x, f x = y ∧ ClusterPt x ℱ