-- 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)
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₂⟩
⊢ ∀ (K : Set X),
    IsCompact K →
      Tendsto (fun i => restrict K (F i)) l
        (𝓝
          (restrict K
            (liftCover' (fun s => ∀ ⦃f : Filter X⦄ [inst : f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))

Tactic:
intro s hs

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
    (𝓝 (restrict s (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 (𝓝 (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

Tactic:
exact hf s hs

Result:
no goals

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:
rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂

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₂
⊢ (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)
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)

Tactic:
have h :
  ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (x : X) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    f s₁ hs₁ ⟨x, hxs₁⟩ = f s₂ hs₂ ⟨x, hxs₂⟩ := by
  rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
  haveI := isCompact_iff_compactSpace.mp hs₁
  haveI := isCompact_iff_compactSpace.mp hs₂
  have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
  have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
  exact tendsto_nhds_unique h₁ 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))
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)

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, Tendsto F l (𝓝 f)) ↔ ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i => restrict s (F i)) l (𝓝 f)

Tactic:
constructor

Result:
case mp
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, Tendsto F l (𝓝 f)) → ∀ (s : Set X), IsCompact s → ∃ f, Tendsto (fun i => restrict s (F i)) l (𝓝 f)

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)

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₁
⊢ (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₁
this : CompactSpace ↑s₂
⊢ (f s₁ hs₁) ⟨x, hxs₁⟩ = (f s₂ hs₂) ⟨x, hxs₂⟩