-- Mathlib/Topology/Compactness/Compact.lean
theorem isClosedMap_snd_of_compactSpace [CompactSpace X] :
    IsClosedMap (Prod.snd : X × Y → Y) := fun s hs => by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro y hy
  have : univ ×ˢ {y} ⊆ sᶜ

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y

Tactic:
rcases generalized_tube_lemma isCompact_univ isCompact_singleton hs.isOpen_compl this
  with ⟨U, V, -, hVo, hU, hV, hs⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
⊢ IsClosed (Prod.snd '' s)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
⊢ ∀ x ∈ (Prod.snd '' s)ᶜ, (Prod.snd '' s)ᶜ ∈ 𝓝 x

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y

Tactic:
have : univ ×ˢ {y} ⊆ sᶜ := by
  exact fun (x, y') ⟨_, rfl⟩ hs => hy ⟨(x, y'), hs, rfl⟩

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
⊢ ∀ x ∈ (Prod.snd '' s)ᶜ, (Prod.snd '' s)ᶜ ∈ 𝓝 x

Tactic:
intro y hy

Result:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ V ⊆ (Prod.snd '' s)ᶜ

Tactic:
rintro _ hzV ⟨z, hzs, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
z : X × Y
hzs : z ∈ s
hzV : z.2 ∈ V
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
z : X × Y
hzs : z ∈ s
hzV : z.2 ∈ V
⊢ False

Tactic:
exact hs ⟨hU trivial, hzV⟩ hzs

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ (Prod.snd '' s)ᶜ ∈ 𝓝 y

Tactic:
refine mem_nhds_iff.2 ⟨V, ?_, hVo, hV rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs✝ : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
this : univ ×ˢ {y} ⊆ sᶜ
U : Set X
V : Set Y
hVo : IsOpen V
hU : univ ⊆ U
hV : {y} ⊆ V
hs : U ×ˢ V ⊆ sᶜ
⊢ V ⊆ (Prod.snd '' s)ᶜ

Proof state:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
s : Set (X × Y)
hs : IsClosed s
y : Y
hy : y ∈ (Prod.snd '' s)ᶜ
⊢ univ ×ˢ {y} ⊆ sᶜ

Tactic:
exact fun (x, y') ⟨_, rfl⟩ hs => hy ⟨(x, y'), hs, rfl⟩

Result:
no goals