case mp
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) → ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)) → ∃ f, Filter.Tendsto F l (𝓝 f)
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) ↔ ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
constructor
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : C(α, β)
hf : Filter.Tendsto F l (𝓝 f)
s : Set α
hs✝ : IsCompact s
⊢ ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∃ f, Filter.Tendsto F l (𝓝 f)) → ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
rintro ⟨f, hf⟩ s _
no goals
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : C(α, β)
hf : Filter.Tendsto F l (𝓝 f)
s : Set α
hs✝ : IsCompact s
⊢ ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
h : ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
⊢ (∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)) → ∃ f, Filter.Tendsto F l (𝓝 f)
intro h
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
h : ∀ (s : Set α), IsCompact s → ∃ f, Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 f)
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
choose f hf using h
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
have h :
  ∀ (s₁) (hs₁ : IsCompact s₁) (s₂) (hs₂ : IsCompact s₂) (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₂
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
have hs : ∀ x : α, ∃ (s : _), IsCompact s ∧ s ∈ 𝓝 x := by
  intro x
  obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x
  exact ⟨s, hs, hs'⟩
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ Filter.Tendsto F l
    (𝓝
      (liftCover'
        (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
        (fun s hs => f s hs) h hs))
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∃ f, Filter.Tendsto F l (𝓝 f)
refine ⟨liftCover' _ _ h hs, ?_⟩
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∀ (s : Set α),
    IsCompact s →
      Filter.Tendsto (fun i => restrict s (F i)) l
        (𝓝
          (restrict s
            (liftCover'
              (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
              (fun s hs => f s hs) h hs)))
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ Filter.Tendsto F l
    (𝓝
      (liftCover'
        (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
        (fun s hs => f s hs) h hs))
rw [tendsto_compactOpen_iff_forall]
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l
    (𝓝
      (restrict s
        (liftCover'
          (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
          (fun s hs => f s hs) h hs✝)))
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
⊢ ∀ (s : Set α),
    IsCompact s →
      Filter.Tendsto (fun i => restrict s (F i)) l
        (𝓝
          (restrict s
            (liftCover'
              (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
              (fun s hs => f s hs) h hs)))
intro s hs
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s ?m.40109))

α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ s ∈ fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l
    (𝓝
      (restrict s
        (liftCover'
          (fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f)
          (fun s hs => f s hs) h hs✝)))
rw [liftCover_restrict']
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s ?m.40109))

α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
hs✝ : ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
s : Set α
hs : IsCompact s
⊢ s ∈ fun s => ∀ ⦃f : Filter α⦄ [inst : Filter.NeBot f], f ≤ Filter.principal s → ∃ a, a ∈ s ∧ ClusterPt a f
exact hf s hs
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
⊢ ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
rintro s₁ hs₁ s₂ hs₂ x hxs₁ hxs₂
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this : CompactSpace ↑s₁
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
haveI := isCompact_iff_compactSpace.mp hs₁
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this : CompactSpace ↑s₁
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
haveI := isCompact_iff_compactSpace.mp hs₂
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
have h₁ := (continuous_eval_const' (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
h₂ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₂ }) ∘ fun i => restrict s₂ (F i)) l
    (𝓝 (↑(f s₂ hs₂) { val := x, property := hxs₂ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
have h₂ := (continuous_eval_const' (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
s₁ : Set α
hs₁ : IsCompact s₁
s₂ : Set α
hs₂ : IsCompact s₂
x : α
hxs₁ : x ∈ s₁
hxs₂ : x ∈ s₂
this✝ : CompactSpace ↑s₁
this : CompactSpace ↑s₂
h₁ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₁ }) ∘ fun i => restrict s₁ (F i)) l
    (𝓝 (↑(f s₁ hs₁) { val := x, property := hxs₁ }))
h₂ :
  Filter.Tendsto ((fun f => ↑f { val := x, property := hxs₂ }) ∘ fun i => restrict s₂ (F i)) l
    (𝓝 (↑(f s₂ hs₂) { val := x, property := hxs₂ }))
⊢ ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
exact tendsto_nhds_unique h₁ h₂
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
⊢ ∀ (x : α), ∃ s, IsCompact s ∧ s ∈ 𝓝 x
intro x
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
s : Set α
hs : IsCompact s
hs' : s ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
obtain ⟨s, hs, hs'⟩ := exists_compact_mem_nhds x
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.37922
inst✝⁶ : TopologicalSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : TopologicalSpace γ
inst✝³ : LocallyCompactSpace α
inst✝² : T2Space α
inst✝¹ : T2Space β
ι : Type u_3
l : Filter ι
inst✝ : Filter.NeBot l
F : ι → C(α, β)
f : (s : Set α) → IsCompact s → C(↑s, β)
hf : ∀ (s : Set α) (hs : IsCompact s), Filter.Tendsto (fun i => restrict s (F i)) l (𝓝 (f s hs))
h :
  ∀ (s₁ : Set α) (hs₁ : IsCompact s₁) (s₂ : Set α) (hs₂ : IsCompact s₂) (x : α) (hxs₁ : x ∈ s₁) (hxs₂ : x ∈ s₂),
    ↑(f s₁ hs₁) { val := x, property := hxs₁ } = ↑(f s₂ hs₂) { val := x, property := hxs₂ }
x : α
s : Set α
hs : IsCompact s
hs' : s ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
exact ⟨s, hs, hs'⟩