awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hf : MapsTo (⇑f : (a : X) → Y) K U
V : Set Y
hVo : IsOpen[inst_1] V
hKV : (⇑f : (a : X) → Y) '' K ⊆ V
hVU : closure[inst_1] V ⊆ U
g : C(X, Y)
hg : Membership.mem (γ := Set C(X, Y)) (closure {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) K V}) g
⊢ MapsTo (⇑(id g) : (a : X) → Y) K U

Tactic:
((isClosed_setOf_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU

Premises used: Set.MapsTo.mono_right, IsClosed.closure_subset, ContinuousMap.isClosed_setOf_mapsTo, isClosed_closure
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hf : MapsTo (⇑f : (a : X) → Y) K U
V : Set Y
hVo : IsOpen[inst_1] V
hKV : (⇑f : (a : X) → Y) '' K ⊆ V
hVU : closure[inst_1] V ⊆ U
g : C(X, Y)
hg : Membership.mem (γ := Set C(X, Y)) (closure {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) K V}) g
h : Membership.mem (γ := Set C(X, Y)) (closure {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (closure[inst_1] V)}) (id g)
⊢ MapsTo (⇑(id g) : (a : X) → Y) K U

Tactic:
refine ((isClosed_setOf_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU

Premises used: Set.MapsTo.mono_right, IsClosed.closure_subset, ContinuousMap.isClosed_setOf_mapsTo, isClosed_closure
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hf : MapsTo (⇑f : (a : X) → Y) K U
V : Set Y
hVo : IsOpen[inst_1] V
hKV : (⇑f : (a : X) → Y) '' K ⊆ V
hVU : closure[inst_1] V ⊆ U
g : C(X, Y)
hg : Membership.mem (γ := Set C(X, Y)) (closure {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) K V}) g
⊢ Membership.mem (γ := Set C(X, Y)) (closure {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (closure[inst_1] V)}) (id g)

Tactic:
closure_mono (fun _ h ↦ h.mono_right subset_closure) hg

Premises used: closure_mono
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hf : MapsTo (⇑f : (a : X) → Y) K U
V : Set Y
hVo : IsOpen[inst_1] V
hKV : (⇑f : (a : X) → Y) '' K ⊆ V
hVU : closure[inst_1] V ⊆ U
g : C(X, Y)
hg : Membership.mem (γ := Set C(X, Y)) (closure {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) K V}) g
⊢ Membership.mem (γ := Set C(X, Y)) (closure {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (closure[inst_1] V)}) (id g)

Tactic:
exact closure_mono (fun _ h ↦ h.mono_right subset_closure) hg

Premises used: closure_mono
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : T3Space Y
⊢ T3Space C(X, Y)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology X
⊢ Eq (α := (a : C(X, Y)) → X → Y) (⇑homeoFnOfDiscrete : (a : C(X, Y)) → X → Y) (DFunLike.coe (β := fun (a : X) ↦ Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology X
f : X → Y
⊢ (⇑((Homeomorph.symm homeoFnOfDiscrete : (a : X → Y) → C(X, Y)) f : C(X, Y)) : (a : X) → Y) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : DiscreteTopology X
⊢ IsHomeomorph (X := C(X, Y)) (Y := (a : X) → Y) (DFunLike.coe (β := fun (x : X) ↦ Y))

Tactic:
homeoFnOfDiscrete.isHomeomorph

Premises used: ContinuousMap.homeoFnOfDiscrete, Homeomorph.isHomeomorph
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
⊢ Continuous (Y := ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y) fun (F : C(X, Y)) ↦ restrict s F

Tactic:
continuous_precomp <| restrict s <| .id X

Premises used: ContinuousMap.comp, ContinuousMap.id, ContinuousMap.continuous_precomp, ContinuousMap.restrict
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
⊢ LE.le (α := TopologicalSpace C(X, Y)) compactOpen (induced (restrict s) compactOpen)

Tactic:
(continuous_restrict s).le_induced

Premises used: ContinuousMap.continuous_restrict, Continuous.le_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ Eq (α := TopologicalSpace C(X, Y)) compactOpen (⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen)

Tactic:
le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_

Premises used: le_iInf₂, le_antisymm, ContinuousMap.compactOpen_le_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
refine :
  LE.le (α := TopologicalSpace C(X, Y)) (⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen)
    compactOpen
⊢ Eq (α := TopologicalSpace C(X, Y)) compactOpen (⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen)

Tactic:
refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_

Premises used: le_iInf₂, le_antisymm, ContinuousMap.compactOpen_le_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
⊢ LE.le (α := TopologicalSpace C(X, Y)) (⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen)
    compactOpen

Tactic:
le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_

Premises used: Iff.mpr, Set.forall_mem_image2, le_generateFrom
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
refine :
  ∀ (K : Set X) (hK : IsCompact K) (U : Set Y)
    (hU : Membership.mem (γ := Set (Set Y)) {U : Set Y | IsOpen[inst_1] U} U),
    IsOpen[⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen]
      {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}
⊢ LE.le (α := TopologicalSpace C(X, Y)) (⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen)
    compactOpen

Tactic:
refine le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_

Premises used: Iff.mpr, Set.forall_mem_image2, le_generateFrom
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : Membership.mem (γ := Set (Set Y)) {U : Set Y | IsOpen[inst_1] U} U
⊢ IsOpen[⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen]
    {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}

Tactic:
TopologicalSpace.le_def.1 (iInf₂_le K hK) _ ?_

Premises used: iInf₂_le, TopologicalSpace.le_def, Iff.mp
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : Membership.mem (γ := Set (Set Y)) {U : Set Y | IsOpen[inst_1] U} U
refine : IsOpen[induced (restrict K) compactOpen] {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}
⊢ IsOpen[⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen]
    {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}

Tactic:
refine TopologicalSpace.le_def.1 (iInf₂_le K hK) _ ?_

Premises used: iInf₂_le, TopologicalSpace.le_def, Iff.mp
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : Membership.mem (γ := Set (Set Y)) {U : Set Y | IsOpen[inst_1] U} U
⊢ IsOpen[induced (restrict K) compactOpen]
    (restrict K ⁻¹'
      {f : ContinuousMap.{u_2, u_3} (↑K : Type u_2) Y |
        MapsTo.{u_2, u_3} (α := (↑K : Type u_2)) (⇑f : (a : (↑K : Type u_2)) → Y) univ U})

Tactic:
isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)

Premises used: ContinuousMap.isOpen_setOf_mapsTo, isCompact_iff_isCompact_univ, isOpen_induced, Iff.mp
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : Membership.mem (γ := Set (Set Y)) {U : Set Y | IsOpen[inst_1] U} U
h :
  Eq (α := Set C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}
    (restrict K ⁻¹'
      {f : ContinuousMap.{u_2, u_3} (↑K : Type u_2) Y |
        MapsTo.{u_2, u_3} (α := (↑K : Type u_2)) (⇑f : (a : (↑K : Type u_2)) → Y) univ U})
⊢ IsOpen[induced (restrict K) compactOpen] {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}

Tactic:
convert! isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)

Premises used: ContinuousMap.isOpen_setOf_mapsTo, isCompact_iff_isCompact_univ, isOpen_induced, Iff.mp
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Set X
hK : IsCompact K
U : Set Y
hU : Membership.mem (γ := Set (Set Y)) {U : Set Y | IsOpen[inst_1] U} U
⊢ Eq (α := Set C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}
    (restrict K ⁻¹'
      {f : ContinuousMap.{u_2, u_3} (↑K : Type u_2) Y |
        MapsTo.{u_2, u_3} (α := (↑K : Type u_2)) (⇑f : (a : (↑K : Type u_2)) → Y) univ U})

Tactic:
simp [Subtype.forall, MapsTo]

Premises used: Subtype.forall, Set.MapsTo
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
rw : 𝓝 f = ⨅ (s : Set X), ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))
⊢ 𝓝 f = ⨅ (s : Set X), ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))

Tactic:
rw [compactOpen_eq_iInf_induced]

Premises used: ContinuousMap.compactOpen_eq_iInf_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ (s : Set X), ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))

Tactic:
simp only [nhds_iInf, nhds_induced]

Premises used: nhds_iInf, nhds_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
ι : Type u_6
l : Filter ι
F : ι → C(X, Y)
f : C(X, Y)
hFf : Tendsto F l (𝓝 f)
s : Set X
⊢ Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (restrict s f))

Tactic:
(continuous_restrict s).continuousAt.tendsto.comp hFf

Premises used: Continuous.continuousAt, ContinuousMap.continuous_restrict, ContinuousAt.tendsto, Filter.Tendsto.comp, ContinuousMap.restrict
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
ι : Type u_6
l : Filter ι
F : ι → C(X, Y)
f : C(X, Y)
rw : Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun (i : ι) ↦ restrict K (F i)) l (𝓝 (restrict K f))
⊢ Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun (i : ι) ↦ restrict K (F i)) l (𝓝 (restrict K f))

Tactic:
rw [compactOpen_eq_iInf_induced]

Premises used: ContinuousMap.compactOpen_eq_iInf_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
ι : Type u_6
l : Filter ι
F : ι → C(X, Y)
f : C(X, Y)
⊢ Tendsto F l (𝓝 f) ↔ ∀ (K : Set X), IsCompact K → Tendsto (fun (i : ι) ↦ restrict K (F i)) l (𝓝 (restrict K f))

Tactic:
simp [nhds_iInf, nhds_induced, Filter.tendsto_comap_iff, Function.comp_def]

Premises used: nhds_iInf, Filter.tendsto_comap_iff, Function.comp_def, nhds_induced
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
mp :
  (∃ (f : C(X, Y)), Tendsto F l (𝓝 f)) →
    ∀ (s : Set X),
      IsCompact s → ∃ (f : ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 f)
mpr :
  (∀ (s : Set X),
      IsCompact s →
        ∃ (f : ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 f)) →
    ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)
⊢ (∃ (f : C(X, Y)), Tendsto F l (𝓝 f)) ↔
    ∀ (s : Set X),
      IsCompact s → ∃ (f : ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 f)

Tactic:
constructor
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : C(X, Y)
hf : Tendsto F l (𝓝 f)
s : Set X
h : IsCompact s
⊢ ∃ (f : ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 f)

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

Premises used: ContinuousMap.tendsto_compactOpen_restrict, Exists.intro, ContinuousMap.restrict
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : C(X, Y)
hf : Tendsto F l (𝓝 f)
s : Set X
h : IsCompact s
⊢ ∃ (f : ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 f)

Tactic:
exact ⟨f.restrict s, tendsto_compactOpen_restrict hf s⟩
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
h :
  ∀ (s : Set X),
    IsCompact s → ∃ (f : ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 f)
mpr :
  ∀ (f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) Y)
    (hf : ∀ (s : Set X) (a : IsCompact s), Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s a))),
    ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)
⊢ ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)

Tactic:
choose f hf using h
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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₂
⊢ CompactSpace.{u_2} (↑s₁ : Type u_2)

Tactic:
haveI := isCompact_iff_compactSpace.mp hs₁
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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.{u_2} (↑s₁ : Type u_2)
⊢ CompactSpace.{u_2} (↑s₂ : Type u_2)

Tactic:
haveI := isCompact_iff_compactSpace.mp hs₂
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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_1 : CompactSpace.{u_2} (↑s₁ : Type u_2)
this : CompactSpace.{u_2} (↑s₂ : Type u_2)
⊢ Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₁ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) ∘
        fun (i : ι) ↦ restrict s₁ (F i) :
      ι → Y)
    l (𝓝 ((f s₁ hs₁ : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) : Filter Y)

Tactic:
have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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_1 : CompactSpace.{u_2} (↑s₁ : Type u_2)
this : CompactSpace.{u_2} (↑s₂ : Type u_2)
h₁ :
  Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₁ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) ∘
        fun (i : ι) ↦ restrict s₁ (F i) :
      ι → Y)
    l (𝓝 ((f s₁ hs₁ : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) : Filter Y)
⊢ Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₂ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₂ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂)) ∘
        fun (i : ι) ↦ restrict s₂ (F i) :
      ι → Y)
    l (𝓝 ((f s₂ hs₂ : (a : { x : X // x ∈ s₂ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂)) : Filter Y)

Tactic:
have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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_1 : CompactSpace.{u_2} (↑s₁ : Type u_2)
this : CompactSpace.{u_2} (↑s₂ : Type u_2)
h₁ :
  Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₁ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) ∘
        fun (i : ι) ↦ restrict s₁ (F i) :
      ι → Y)
    l (𝓝 ((f s₁ hs₁ : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) : Filter Y)
h₂ :
  Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₂ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₂ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂)) ∘
        fun (i : ι) ↦ restrict s₂ (F i) :
      ι → Y)
    l (𝓝 ((f s₂ hs₂ : (a : { x : X // x ∈ s₂ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂)) : Filter Y)
⊢ Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
    ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)

Tactic:
tendsto_nhds_unique h₁ h₂

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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_1 : CompactSpace.{u_2} (↑s₁ : Type u_2)
this : CompactSpace.{u_2} (↑s₂ : Type u_2)
h₁ :
  Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₁ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) ∘
        fun (i : ι) ↦ restrict s₁ (F i) :
      ι → Y)
    l (𝓝 ((f s₁ hs₁ : (a : { x : X // x ∈ s₁ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁)) : Filter Y)
h₂ :
  Tendsto.{u_6, u_3} (β := Y)
    ((fun (f : ContinuousMap.{u_2, u_3} (↑s₂ : Type u_2) Y) ↦
          (f : (a : { x : X // x ∈ s₂ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂)) ∘
        fun (i : ι) ↦ restrict s₂ (F i) :
      ι → Y)
    l (𝓝 ((f s₂ hs₂ : (a : { x : X // x ∈ s₂ }) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂)) : Filter Y)
⊢ Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
    ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)

Tactic:
exact tendsto_nhds_unique h₁ h₂

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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₂),
    Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
      ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)

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₂
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : WeaklyLocallyCompactSpace X
inst_3 : T2Space Y
ι : Type u_6
l : Filter ι
inst_4 : l.NeBot
F : ι → C(X, Y)
f : (s : Set X) → IsCompact s → ContinuousMap.{u_2, u_3} (↑s : Type u_2) 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₂),
    Eq.{u_3 + 1} (α := Y) ((f s₁ hs₁ : (a : (↑s₁ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₁) x hxs₁) : Y)
      ((f s₂ hs₂ : (a : (↑s₂ : Type u_2)) → Y) (Subtype.mk (p := fun (x : X) ↦ x ∈ s₂) x hxs₂) : Y)
⊢ ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)

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

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, ContinuousMap.liftCover', Exists.intro