awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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).HasBasis
    (fun (S : Set (Prod.{u_2, u_3} (Set X) (Set Y))) ↦
      S.Finite ∧ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑f : (a : X) → Y) K U)
    fun (x : Set (Prod.{u_2, u_3} (Set X) (Set Y))) ↦ ⋂ KU ∈ x, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) KU.1 KU.2}
have refine : ∀ (s : Set C(X, Y)),
  s ∈ 𝓝 f ↔
    ∃ (i : Set (Prod.{u_2, u_3} (Set X) (Set Y))),
      (i.Finite ∧
          ∀ (K : Set X) (U : Set Y), (K, U) ∈ i → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑f : (a : X) → Y) K U) ∧
        ⋂ KU ∈ i, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) KU.1 KU.2} ⊆ s
Tactic: refine ⟨fun 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
f : C(X, Y)
s : Set C(X, Y)
⊢ s ∈ 𝓝 f ↔
    ∃ (i : Set (Prod.{u_2, u_3} (Set X) (Set Y))),
      (i.Finite ∧
          ∀ (K : Set X) (U : Set Y), (K, U) ∈ i → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑f : (a : X) → Y) K U) ∧
        ⋂ KU ∈ i, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) KU.1 KU.2} ⊆ s
have simp_rw : Membership.mem (γ := Filter C(X, Y))
    (⨅ (x : Prod.{u_2, u_3} (Set X) (Set Y)),
      ⨅ (_ : IsCompact x.1 ∧ IsOpen[inst_1] x.2 ∧ MapsTo (⇑f : (a : X) → Y) x.1 x.2),
        𝓟 {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) x.1 x.2})
    s ↔
  ∃ (i : Set (Prod.{u_2, u_3} (Set X) (Set Y))),
    (i.Finite ∧
        ∀ (K : Set X) (U : Set Y), (K, U) ∈ i → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑f : (a : X) → Y) K U) ∧
      ⋂ KU ∈ i, {g : C(X, Y) | MapsTo (⇑g : (a : X) → Y) KU.1 KU.2} ⊆ s
Tactic: simp_rw [nhds_compactOpen, iInf_comm.{_, 0, _ + 1}, iInf_prod', iInf_and']
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
⊢ HasBasis (α := C(X, Y)) (𝓝 (const X c)) (fun (Ki : Prod.{u_2, u_6} (Set X) ι) ↦ IsCompact Ki.1 ∧ p Ki.2)
    fun (Ki : Prod.{u_2, u_6} (Set X) ι) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) Ki.1 (U Ki.2)}
have refine_1 : ∀ (s : Set C(X, Y)) (hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s),
  ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
Tactic: refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩⟩
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
refine_1 :
  ∀ (s : Set C(X, Y)) (hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s),
    ∃ (i : Prod.{u_2, u_6} (Set X) ι),
      (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
⊢ HasBasis (α := C(X, Y)) (𝓝 (const X c)) (fun (Ki : Prod.{u_2, u_6} (Set X) ι) ↦ IsCompact Ki.1 ∧ p Ki.2)
    fun (Ki : Prod.{u_2, u_6} (Set X) ι) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) Ki.1 (U Ki.2)}
have refine_2 : ∀ (s : Set C(X, Y))
  (hs :
    ∃ (i : Prod.{u_2, u_6} (Set X) ι),
      (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s),
  Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
Tactic: refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩⟩
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have refine_1 : ∀ (S : Set (Prod.{u_2, u_3} (Set X) (Set Y))) (hSf : S.Finite)
  (hS :
    ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑(const X c) : (a : X) → Y) K U)
  (hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s),
  ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
Tactic: rcases ContinuousMap.mem_nhds_iff.mp hs with ⟨S, hSf, hS, hSsub⟩
-- 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
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hS : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑(const X c) : (a : X) → Y) K U
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
Tactic: choose hScompact hSopen hSmaps using hS
Cleared hypotheses: 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
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hS : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑(const X c) : (a : X) → Y) K U
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
Tactic: choose hScompact hSopen hSmaps using hS
Cleared hypotheses: 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
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hS : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen[inst_1] U ∧ MapsTo (⇑(const X c) : (a : X) → Y) K U
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
Tactic: choose hScompact hSopen hSmaps using hS
Cleared hypotheses: hS
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
⊢ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
have simp : ∀ (a : Set X) (b : Set Y), (a, b) ∈ S → ∀ (i : a.Nonempty), b ∈ 𝓝 c
Tactic: simp only [biInter_mem hSf, Prod.forall, iInter_mem]
-- 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
ι : Type u_6
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
Tactic: have : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c := by
      simp only [biInter_mem hSf, Prod.forall, iInter_mem]
      rintro K U hKU ⟨x, hx⟩
      exact (hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have refine_1 : ∀ (i : ι) (hpi : p i) (hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2),
  ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
Tactic: rcases h.mem_iff.mp this with ⟨i, hpi, hi⟩
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
⊢ ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
have refine_1 : Subset (α := Set C(X, Y))
  {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)}
  {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U}
Tactic: refine ⟨(⋃ KU ∈ S, KU.1, i), ⟨hSf.isCompact_biUnion <| Prod.forall.2 hScompact, hpi⟩,
      Subset.trans ?_ hSsub⟩
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf :
  Membership.mem (γ := Set C(X, Y))
    {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)} f
K : Set X
V : Set Y
hKV : (K, V) ∈ S
⊢ MapsTo (⇑f : (a : X) → Y) K V
have refine_1 : ∀ (hKV : (∅, V) ∈ S), MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) ∅ V
Tactic: rcases K.eq_empty_or_nonempty with rfl | hKne
Cleared hypotheses: K, hKV
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf :
  Membership.mem (γ := Set C(X, Y))
    {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)} f
K : Set X
V : Set Y
hKV : (K, V) ∈ S
refine_1 : ∀ (hKV : (∅, V) ∈ S), MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) ∅ V
⊢ MapsTo (⇑f : (a : X) → Y) K V
have refine_1₁ : ∀ (hKne : K.Nonempty), MapsTo (⇑f : (a : X) → Y) K V
Tactic: rcases K.eq_empty_or_nonempty with rfl | hKne
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs : Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
S : Set (Prod.{u_2, u_3} (Set X) (Set Y))
hSf : S.Finite
hSsub : {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s
hScompact : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K
hSopen : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U
hSmaps : ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑(const X c) : (a : X) → Y) K U
this : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c
i : ι
hpi : p i
hi : U i ⊆ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2
f : C(X, Y)
hf :
  Membership.mem (γ := Set C(X, Y))
    {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) (⋃ KU ∈ S, KU.1, i).1 (U (⋃ KU ∈ S, KU.1, i).2)} f
K : Set X
V : Set Y
hKV : (K, V) ∈ S
hKne : K.Nonempty
⊢ MapsTo (⇑f : (a : X) → Y) K V
have refine_1 : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ⊆ V
Tactic: refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
hs :
  ∃ (i : Prod.{u_2, u_6} (Set X) ι), (IsCompact i.1 ∧ p i.2) ∧ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) i.1 (U i.2)} ⊆ s
⊢ Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
have refine_2 : ∀ (K : Set X) (i : ι) (hi : {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) (K, i).1 (U (K, i).2)} ⊆ s)
  (hK : IsCompact (K, i).1) (hpi : p (K, i).2), Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
Tactic: rcases hs with ⟨⟨K, i⟩, ⟨hK, hpi⟩, hi⟩
Cleared hypotheses: hs
-- 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
c : Y
p : ι → Prop
U : ι → Set Y
h : (𝓝 c).HasBasis p U
s : Set C(X, Y)
K : Set X
i : ι
hi : {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) (K, i).1 (U (K, i).2)} ⊆ s
hK : IsCompact (K, i).1
hpi : p (K, i).2
⊢ Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s
have h₁ : ∀ (f : C(X, Y)) (hf : MapsTo (⇑f : (a : X) → Y) K (interior (U i))), f ∈ s
Tactic: filter_upwards [eventually_mapsTo hK isOpen_interior fun x _ ↦
      mem_interior_iff_mem_nhds.mpr <| h.mem_of_mem hpi] with f hf
-- 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
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : X × C(Y, Z)) ↦ prodMk (const Y p.1) p.2
have simp_rw : ∀ (x : X × C(Y, Z)) (K : Set Y),
  IsCompact K →
    ∀ (U : Set (X × Z)),
      IsOpen[instTopologicalSpaceProd] U →
        MapsTo (⇑(prodMk (const Y x.1) x.2) : (a : Y) → X × Z) K U →
          ∀ᶠ (a : X × C(Y, Z)) in 𝓝 x, MapsTo (⇑(prodMk (const Y a.1) a.2) : (a : Y) → X × Z) K U
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt, ContinuousMap.tendsto_nhds_compactOpen]
-- 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
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑(prodMk (const Y (r, f).1) (r, f).2) : (a : Y) → X × Z) K U
⊢ ∀ᶠ (a : X × C(Y, Z)) in 𝓝 (r, f), MapsTo (⇑(prodMk (const Y a.1) a.2) : (a : Y) → X × Z) K U
have obtain : ∀ (V : Set X) (W : Set Z) (hV : IsOpen[inst] V) (hW : IsOpen[inst_2] W) (hrV : {r} ⊆ V)
  (hKW : (⇑f : (a : Y) → Z) '' K ⊆ W) (hVW : V ×ˢ W ⊆ U),
  ∀ᶠ (a : X × C(Y, Z)) in 𝓝 (r, f), MapsTo (⇑(prodMk (const Y a.1) a.2) : (a : Y) → X × Z) K U
Tactic: obtain ⟨V, W, hV, hW, hrV, hKW, hVW⟩ := generalized_tube_lemma (isCompact_singleton (x := r))
    (hK.image f.continuous) hU (by simpa [Set.subset_def, forall_comm (α := X)])
-- 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
r : X
f : C(Y, Z)
K : Set Y
hK : IsCompact K
U : Set (X × Z)
hU : IsOpen[instTopologicalSpaceProd] U
H : MapsTo (⇑(prodMk (const Y (r, f).1) (r, f).2) : (a : Y) → X × Z) K U
V : Set X
W : Set Z
hV : IsOpen[inst] V
hW : IsOpen[inst_2] W
hrV : {r} ⊆ V
hKW : (⇑f : (a : Y) → Z) '' K ⊆ W
hVW : V ×ˢ W ⊆ U
⊢ ∀ᶠ (a : X × C(Y, Z)) in 𝓝 (r, f), MapsTo (⇑(prodMk (const Y a.1) a.2) : (a : Y) → X × Z) K U
have refine : ∀ x ∈ SProd.sprod (β := Set C(Y, Z)) V {x : C(Y, Z) | (fun (g : C(Y, Z)) ↦ MapsTo (⇑g : (a : Y) → Z) K W) x},
  MapsTo (⇑(prodMk (const Y x.1) x.2) : (a : Y) → X × Z) K U
Tactic: refine Filter.eventually_of_mem (prod_mem_nhds (hV.mem_nhds (by simpa using hrV))
    (ContinuousMap.eventually_mapsTo hK hW (Set.mapsTo_iff_image_subset.mpr hKW))) ?_
-- 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 : LocallyCompactPair Y Z
⊢ Continuous (Y := C(X, Z)) fun (x : C(X, Y) × C(Y, Z)) ↦ x.2.comp x.1
have simp_rw : ∀ (x : C(X, Y) × C(Y, Z)) (K : Set X),
  IsCompact K →
    ∀ (U : Set Z),
      IsOpen[inst_2] U →
        MapsTo (⇑(x.2.comp x.1) : (a : X) → Z) K U →
          ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 x, MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_compactOpen]
-- 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 : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst_2] U
⊢ MapsTo (⇑((f, g).2.comp (f, g).1) : (a : X) → Z) K U →
    ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
have MapsTo : ∀ (hKU : MapsTo (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := Y) (⇑g : (a : Y) → Z) (⇑f : (a : X) → Y)) K U),
  ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
Tactic: (hKU : MapsTo (g ∘ f) K U)
-- 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 : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst_2] U
hKU : MapsTo (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := Y) (⇑g : (a : Y) → Z) (⇑f : (a : X) → Y)) K U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
have obtain : ∀ (L : Set Y) (hKL : Membership.mem (γ := Filter Y) (𝓝ˢ ((⇑f : (a : X) → Y) '' K)) L) (hLc : IsCompact L)
  (hLU : MapsTo (⇑g : (a : Y) → Z) L U),
  ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
Tactic: obtain ⟨L, hKL, hLc, hLU⟩ : ∃ L ∈ 𝓝ˢ (f '' K), IsCompact L ∧ MapsTo g L U :=
    exists_mem_nhdsSet_isCompact_mapsTo g.continuous (hK.image f.continuous) hU
      (mapsTo_image_iff.2 hKU)
-- Lean 4 proof step from Mathlib.Topology.CompactOpen (hypothesis)
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 : LocallyCompactPair Y Z
f : C(X, Y)
g : C(Y, Z)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst_2] U
hKU : MapsTo (Function.comp.{u_2 + 1, u_3 + 1, u_4 + 1} (β := Y) (⇑g : (a : Y) → Z) (⇑f : (a : X) → Y)) K U
L : Set Y
hKL : Membership.mem (γ := Filter Y) (𝓝ˢ ((⇑f : (a : X) → Y) '' K)) L
hLc : IsCompact L
hLU : MapsTo (⇑g : (a : Y) → Z) L U
⊢ ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
have hKL₁ : MapsTo (⇑f : (a : X) → Y) K (interior L)
Tactic: rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL
Cleared hypotheses: hKL, hLc, hLU
-- 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 : LocallyCompactPair X Y
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (fx : C(X, Y) × X) ↦ (fx.1 : (a : X) → Y) fx.2
have simp_rw : ∀ (x : C(X, Y) × X) (i : Set Y),
  Membership.mem (α := Y) i ((x.1 : (a : X) → Y) x.2 : Y) ∧ IsOpen[inst_1] i →
    ∀ᶠ (x : C(X, Y) × X) in 𝓝 x, Membership.mem (α := Y) i ((x.1 : (a : X) → Y) x.2 : Y)
Tactic: simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]
-- 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_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
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), Membership.mem (α := Y) U ((x.1 : (a : X) → Y) x.2 : Y)
have rcases : ∀ (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)
Tactic: rcases exists_mem_nhds_isCompact_mapsTo f.continuous (hU.mem_nhds hx) with ⟨K, hxK, hK, hKU⟩