-- Mathlib/Topology/CompactOpen.lean
theorem continuous_coev : Continuous (coev X Y)

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
x : Y
K : Set X
hK : IsCompact K
U : Set (Y × X)
hU : IsOpen U
hKU : {x} ×ˢ K ⊆ U
V : Set Y
W : Set X
hV : IsOpen V
hxV : {x} ⊆ V
hKW : K ⊆ W
hVWU : V ×ˢ W ⊆ U
⊢ ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U

Tactic:
filter_upwards [hV.mem_nhds (hxV rfl)] with a ha

Result:
case h
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
x : Y
K : Set X
hK : IsCompact K
U : Set (Y × X)
hU : IsOpen U
hKU : {x} ×ˢ K ⊆ U
V : Set Y
W : Set X
hV : IsOpen V
hxV : {x} ⊆ V
hKW : K ⊆ W
hVWU : V ×ˢ W ⊆ U
a : Y
ha : a ∈ V
⊢ {a} ×ˢ K ⊆ U

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ Continuous (coev X Y)

Tactic:
have : ∀ {a K U}, MapsTo (coev X Y a) K U ↔ {a} ×ˢ K ⊆ U := by simp [mapsTo']

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
⊢ Continuous (coev X Y)

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U

Tactic:
simp [mapsTo']

Result:
no goals

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
⊢ Continuous (coev X Y)

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen, this]

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
⊢ ∀ (x : Y) (K : Set X), IsCompact K → ∀ (U : Set (Y × X)), IsOpen U → {x} ×ˢ K ⊆ U → ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
x : Y
K : Set X
hK : IsCompact K
U : Set (Y × X)
hU : IsOpen U
hKU : {x} ×ˢ K ⊆ U
⊢ ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U

Tactic:
rcases generalized_tube_lemma isCompact_singleton hK hU hKU with ⟨V, W, hV, -, hxV, hKW, hVWU⟩

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
x : Y
K : Set X
hK : IsCompact K
U : Set (Y × X)
hU : IsOpen U
hKU : {x} ×ˢ K ⊆ U
V : Set Y
W : Set X
hV : IsOpen V
hxV : {x} ⊆ V
hKW : K ⊆ W
hVWU : V ×ˢ W ⊆ U
⊢ ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
⊢ ∀ (x : Y) (K : Set X), IsCompact K → ∀ (U : Set (Y × X)), IsOpen U → {x} ×ˢ K ⊆ U → ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U

Tactic:
intro x K hK U hU hKU

Result:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
x : Y
K : Set X
hK : IsCompact K
U : Set (Y × X)
hU : IsOpen U
hKU : {x} ×ˢ K ⊆ U
⊢ ∀ᶠ (a : Y) in 𝓝 x, {a} ×ˢ K ⊆ U

Proof state:
case h
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
this : ∀ {a : Y} {K : Set X} {U : Set (Y × X)}, MapsTo (⇑(coev X Y a)) K U ↔ {a} ×ˢ K ⊆ U
x : Y
K : Set X
hK : IsCompact K
U : Set (Y × X)
hU : IsOpen U
hKU : {x} ×ˢ K ⊆ U
V : Set Y
W : Set X
hV : IsOpen V
hxV : {x} ⊆ V
hKW : K ⊆ W
hVWU : V ×ˢ W ⊆ U
a : Y
ha : a ∈ V
⊢ {a} ×ˢ K ⊆ U

Tactic:
exact (prod_mono (singleton_subset_iff.mpr ha) hKW).trans hVWU

Result:
no goals