-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- If the composition of two continuous functions `f : X → Y` and `g : Y → Z` is proper
and `Y` is T2, then `f` is proper. -/
lemma isProperMap_of_comp_of_t2 [T2Space Y] (hf : Continuous f) (hg : Continuous g)
    (hgf : IsProperMap (g ∘ f)) : IsProperMap f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : Continuous (g ∘ f) ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
rcases hgf.2 ((hg.tendsto y).comp h) with ⟨x, -, hx⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : Continuous (g ∘ f) ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
x : X
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_ultrafilter_of_t2]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
rw [isProperMap_iff_ultrafilter] at hgf

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : Continuous (g ∘ f) ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
⊢ Continuous f ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
refine ⟨hf, fun 𝒰 y h ↦ ?_⟩

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : IsProperMap (g ∘ f)
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
f : X → Y
g : Y → Z
inst✝ : T2Space Y
hf : Continuous f
hg : Continuous g
hgf : Continuous (g ∘ f) ∧ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Z⦄, Tendsto (g ∘ f) (↑𝒰) (𝓝 y) → ∃ x, (g ∘ f) x = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter X
y : Y
h : Tendsto f (↑𝒰) (𝓝 y)
x : X
hx : ↑𝒰 ≤ 𝓝 x
⊢ ∃ x, ↑𝒰 ≤ 𝓝 x

Tactic:
exact ⟨x, hx⟩

Result:
no goals