-- Mathlib/Topology/Maps/Proper/UniversallyClosed.lean
theorem isProperMap_iff_isClosedMap_ultrafilter {X : Type u} {Y : Type v} [TopologicalSpace X]
    [TopologicalSpace Y] {f : X → Y} :
    IsProperMap f ↔ Continuous f ∧ IsClosedMap
      (Prod.map f id : X × Ultrafilter X → Y × Ultrafilter X)

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Tactic:
have := H.2 F isClosed_closure

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Proof state:
case mpr.intro.mk.intro.refl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (nhds (f x))
⊢ ∃ x_1, f x_1 = f x ∧ ↑(id snd✝) ≤ nhds x_1

Tactic:
refine ⟨x, rfl, fun U hU ↦ Ultrafilter.compl_not_mem_iff.mp fun hUc ↦ ?_⟩

Result:
case mpr.intro.mk.intro.refl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
⊢ False

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap (Prod.map f id)

Tactic:
constructor <;> intro H

Result:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)

case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

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

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Proof state:
case mpr.intro.mk.intro.refl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd✝), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
hy : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
⊢ False

Tactic:
rcases hx (U ×ˢ {𝒢 | Uᶜ ∈ 𝒢}) (prod_mem_nhds hU ((ultrafilter_isOpen_basic _).mem_nhds hUc))
  with ⟨⟨y, 𝒢⟩, ⟨⟨hy : y ∈ U, hy' : Uᶜ ∈ 𝒢⟩, rfl : 𝒢 = pure y⟩⟩

Result:
case mpr.intro.mk.intro.refl.intro.mk.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd✝), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
hy✝ : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
y : X
hy : y ∈ U
hy' : Uᶜ ∈ pure y
⊢ False

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter]

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (nhds y) → ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Tactic:
rcases this with ⟨⟨x, _⟩, hx, ⟨_, _⟩⟩

Result:
case mpr.intro.mk.intro.refl
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : (x, snd✝) ∈ F
hy : Tendsto f (↑(id snd✝)) (nhds (f x))
⊢ ∃ x_1, f x_1 = f x ∧ ↑(id snd✝) ≤ nhds x_1

Proof state:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)

Tactic:
exact ⟨H.continuous, H.universally_closed _⟩

Result:
no goals

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Tactic:
have : (y, 𝒰) ∈ Prod.map f id '' F :=
  this.mem_of_tendsto (hy.prod_mk_nhds (Ultrafilter.tendsto_pure_self 𝒰))
    (Eventually.of_forall fun x ↦ ⟨⟨x, pure x⟩, subset_closure rfl, rfl⟩)

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this✝ : IsClosed (Prod.map f id '' F)
this : (y, 𝒰) ∈ Prod.map f id '' F
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Proof state:
case mpr.intro.mk.intro.refl.intro.mk.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
this : IsClosed (Prod.map f id '' F)
x : X
snd✝ : Ultrafilter X
hx : ∀ t ∈ nhds (x, snd✝), (t ∩ {xℱ | xℱ.2 = pure xℱ.1}).Nonempty
hy✝ : Tendsto f (↑(id snd✝)) (nhds (f x))
U : Set X
hU : U ∈ nhds x
hUc : Uᶜ ∈ id snd✝
y : X
hy : y ∈ U
hy' : Uᶜ ∈ pure y
⊢ False

Tactic:
exact hy' hy

Result:
no goals

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x

Tactic:
let F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
𝒰 : Ultrafilter X
y : Y
hy : Tendsto f (↑𝒰) (nhds y)
F : Set (X × Ultrafilter X) := closure {xℱ | xℱ.2 = pure xℱ.1}
⊢ ∃ x, f x = y ∧ ↑𝒰 ≤ nhds x