-- Mathlib/Topology/CompactOpen.lean
theorem exists_tendsto_compactOpen_iff_forall [WeaklyLocallyCompactSpace X] [T2Space Y]
    {ι : Type*} {l : Filter ι} [Filter.NeBot l] (F : ι → C(X, Y)) :
    (∃ f, Filter.Tendsto F l (𝓝 f)) ↔
      ∀ s : Set X, IsCompact s → ∃ f, Filter.Tendsto (fun i => (F i).restrict s) l (𝓝 f)

Proof state:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
⊢ (∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i => restrict s (F i)) l (𝓝 f)) → ∃ f, Tendsto F l (𝓝 f)

Tactic:
intro h

Result:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
h : ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i => restrict s (F i)) l (𝓝 f)
⊢ ∃ f, Tendsto F l (𝓝 f)

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Tactic:
have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)

Result:
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ : Tendsto ((fun f => f ⟨x, hxs₁⟩) ∘ fun i => restrict s₁ (F i)) l (𝓝 ((f s₁ hs₁) ⟨x, hxs₁⟩))
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Proof state:
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Tactic:
haveI := isCompact_iff_compactSpace.mp hs₁

Result:
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
s₁ : Set X
hs₁ : IsCompact s₁
s₂ : Set X
hs₂ : IsCompact s₂
x : X
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this : CompactSpace ↑s₁
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩

Proof state:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
h : ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i => restrict s (F i)) l (𝓝 f)
⊢ ∃ f, Tendsto F l (𝓝 f)

Tactic:
choose f hf using h

Result:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
⊢ ∃ f, Tendsto F l (𝓝 f)

Proof state:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
⊢ ∃ f, Tendsto F l (𝓝 f)

Tactic:
refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩

Result:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
⊢ Tendsto F l (𝓝 (liftCover' (fun s => ∀ ⦃f : Filter X⦄ [inst : f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯))

Proof state:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i => restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun s => ∀ ⦃f : Filter X⦄ [inst : f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))

Tactic:
rw [liftCover_restrict']

Result:
case mpr
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ Tendsto (fun i => restrict s (F i)) l (𝓝 (f s ?m.63252))

X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → C(↑s, Y)
hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun i => restrict s (F i)) l (𝓝 (f s a))
h :
  ∀ (s₁ : Set X) (hs₁ : IsCompact s₁) (s₂ : Set X) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩
s : Set X
hs : IsCompact s
⊢ s ∈ fun s => ∀ ⦃f : Filter X⦄ [inst : f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f

Proof state:
case mp.intro
X : Type u_2
Y : Type u_3
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : WeaklyLocallyCompactSpace X
inst✝¹ : T2Space Y
ι : Type u_6
l : Filter ι
inst✝ : l.NeBot
F : ι → C(X, Y)
f : C(X, Y)
hf : Tendsto F l (𝓝 f)
s : Set X
a✝ : IsCompact s
⊢ ∃ f, Tendsto (fun i => restrict s (F i)) l (𝓝 f)

Tactic:
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩

Result:
no goals