awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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 : LocallyCompactPair X Y
f : C(X, Y)
x : X
U : Set Y
hx : Membership.mem (α := Y) U ((f : (a : X) → Y) x : Y)
hU : IsOpen[inst_1] U
K : Set X
hxK : K ∈ 𝓝 x
hK : IsCompact K
hKU : MapsTo (⇑f : (a : X) → Y) K U
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), Membership.mem (α := Y) U ((x.1 : (a : X) → Y) x.2 : Y)
have h : ∀ (a : C(X, Y) × X),
  Membership.mem (γ := Set (C(X, Y) × X))
    {x : C(X, Y) × X |
      x ∈ SProd.sprod (α := Set C(X, Y)) {x : C(X, Y) | (fun (g : C(X, Y)) ↦ MapsTo (⇑g : (a : X) → Y) K U) x} K →
        Membership.mem (γ := Set (C(X, Y) × X))
          {x : C(X, Y) × X | (fun (x : C(X, Y) × X) ↦ Membership.mem (α := Y) U ((x.1 : (a : X) → Y) x.2 : Y)) x} x}
    a
Tactic: filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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 : LocallyCompactPair X Y
f : C(X, Y)
x : X
U : Set Y
hx : Membership.mem (α := Y) U ((f : (a : X) → Y) x : Y)
hU : IsOpen[inst_1] U
K : Set X
hxK : K ∈ 𝓝 x
hK : IsCompact K
hKU : MapsTo (⇑f : (a : X) → Y) K U
h :
  ∀ (a : C(X, Y) × X),
    Membership.mem (γ := Set (C(X, Y) × X))
      {x : C(X, Y) × X |
        x ∈ SProd.sprod (α := Set C(X, Y)) {x : C(X, Y) | (fun (g : C(X, Y)) ↦ MapsTo (⇑g : (a : X) → Y) K U) x} K →
          Membership.mem (γ := Set (C(X, Y) × X))
            {x : C(X, Y) × X | (fun (x : C(X, Y) × X) ↦ Membership.mem (α := Y) U ((x.1 : (a : X) → Y) x.2 : Y)) x} x}
      a
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), Membership.mem (α := Y) U ((x.1 : (a : X) → Y) x.2 : Y)
have h₁ : ∀ a ∈ SProd.sprod (α := Set C(X, Y)) {x : C(X, Y) | MapsTo (⇑x : (a : X) → Y) K U} K,
  Membership.mem (α := Y) U ((a.1 : (a : X) → Y) a.2 : Y)
Tactic: filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
⊢ Specializes (X := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) ↔ f ⤳ g
have refine : ∀ (h : Specializes (X := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)), f ⤳ g
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
h : Specializes (X := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)
⊢ f ⤳ g
have suffices : ∀ (K : Set X),
  IsCompact K → ∀ (U : Set Y), IsOpen[inst_1] U → MapsTo (⇑g : (a : X) → Y) K U → MapsTo (⇑f : (a : X) → Y) K U
Tactic: suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
    simpa [specializes_iff_pure, nhds_compactOpen]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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 : R0Space Y
f g : C(X, Y)
h : f ⤳ g
⊢ g ⤳ f
have rw : ∀ (h : Specializes (X := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)),
  Specializes (X := (a : X) → Y) (⇑g : (a : X) → Y) (⇑f : (a : X) → Y)
Tactic: rw [← specializes_coe] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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 : RegularSpace Y
f : C(X, Y)
⊢ (𝓝 f).lift' closure ≤ 𝓝 f
have rw : ∀ (K : Set X),
  IsCompact K →
    ∀ (U : Set Y),
      IsOpen[inst_1] U →
        MapsTo (⇑f : (a : X) → Y) K U → ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a) : (a : X) → Y) K U
Tactic: rw [← tendsto_id', tendsto_nhds_compactOpen]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
⊢ ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a) : (a : X) → Y) K U
have rcases : ∀ (V : Set Y) (hVo : IsOpen[inst_1] V) (hKV : (⇑f : (a : X) → Y) '' K ⊆ V) (hVU : closure[inst_1] V ⊆ U),
  ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a) : (a : X) → Y) K U
Tactic: rcases (hK.image f.continuous).exists_isOpen_closure_subset (hU.mem_nhdsSet.2 hf.image_subset)
      with ⟨V, hVo, hKV, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
⊢ ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a) : (a : X) → Y) K U
have h : ∀ (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: filter_upwards [mem_lift' (eventually_mapsTo hK hVo (mapsTo_iff_image_subset.2 hKV))] with g hg
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have h : Membership.mem (γ := Set C(X, Y)) (closure {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K (closure[inst_1] V)}) (id g)
Tactic: refine ((isClosed_setOf_mapsTo isClosed_closure K).closure_subset ?_).mono_right hVU
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
have refine : LE.le (α := TopologicalSpace C(X, Y)) (⨅ (K : Set X), ⨅ (_ : IsCompact K), induced (restrict K) compactOpen) compactOpen
Tactic: refine le_antisymm (le_iInf₂ fun s _ ↦ compactOpen_le_induced s) ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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
have 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}
Tactic: refine le_generateFrom <| forall_mem_image2.2 fun K (hK : IsCompact K) U hU ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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}
have refine : IsOpen[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) _ ?_
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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] {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}
have 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})
Tactic: convert! isOpen_induced (isOpen_setOf_mapsTo (isCompact_iff_isCompact_univ.1 hK) hU)
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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))
have rw : 𝓝 f = ⨅ (s : Set X), ⨅ (_ : IsCompact s), comap (restrict s) (𝓝 (restrict s f))
Tactic: rw [compactOpen_eq_iInf_induced]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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))
have rw : 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]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)), 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
⊢ ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)
have 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)
Tactic: choose f hf using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
have this : CompactSpace.{u_2} (↑s₁ : Type u_2)
Tactic: haveI := isCompact_iff_compactSpace.mp hs₁
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ 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)
have this₁ : CompactSpace.{u_2} (↑s₂ : Type u_2)
Tactic: haveI := isCompact_iff_compactSpace.mp hs₂
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ 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)
have 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)
Tactic: have h₁ := (continuous_eval_const (⟨x, hxs₁⟩ : s₁)).continuousAt.tendsto.comp (hf s₁ hs₁)
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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)
⊢ 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)
have 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)
Tactic: have h₂ := (continuous_eval_const (⟨x, hxs₂⟩ : s₂)).continuousAt.tendsto.comp (hf s₂ hs₂)
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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))
⊢ ∃ (f : C(X, Y)), Tendsto F l (𝓝 f)
have 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)
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₂
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
have mpr : Tendsto F l (𝓝 (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h sorry))
Tactic: refine ⟨liftCover' _ _ h exists_compact_mem_nhds, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
⊢ Tendsto F l (𝓝 (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯))
have mpr : ∀ (K : Set X),
  IsCompact K →
    Tendsto (fun (i : ι) ↦ restrict K (F i)) l
      (𝓝
        (restrict K
          (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h sorry)))
Tactic: rw [tendsto_compactOpen_iff_forall]
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
s : Set X
hs : IsCompact s
⊢ Tendsto (fun (i : ι) ↦ restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))
have mpr : Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s hs))
Tactic: rw [liftCover_restrict']
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
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)
s : Set X
hs : IsCompact s
mpr : Tendsto (fun (i : ι) ↦ restrict s (F i)) l (𝓝 (f s hs))
⊢ Tendsto (fun (i : ι) ↦ restrict s (F i)) l
    (𝓝 (restrict s (liftCover' (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) f h ⋯)))
have rw : Membership.mem (γ := Set (Set X)) (fun (s : Set X) ↦ ∀ ⦃f : Filter X⦄ [f.NeBot], f ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x f) s
Tactic: rw [liftCover_restrict']
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
⊢ Continuous (X := C(X × Y, Z)) curry
have h : Continuous[instTopologicalSpaceProd, _]
  (Function.uncurry fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y)
Tactic: apply continuous_of_continuous_uncurry
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : LocallyCompactSpace (X × Y)
⊢ Continuous[instTopologicalSpaceProd, _]
    (Function.uncurry fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y)
have h : Continuous[instTopologicalSpaceProd, inst_2]
  (Function.uncurry fun (x : C(X × Y, Z) × X) (y : Y) ↦
    (Function.uncurry (fun (x : C(X × Y, Z)) (y : X) ↦ (x.curry : (a : X) → C(Y, Z)) y) x : (a : Y) → Z) y)
Tactic: apply continuous_of_continuous_uncurry