awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
ι : Type u_6
c : Y
p : ι → Prop
U_1 : ι → Set Y
h : (𝓝 c).HasBasis p U_1
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
K : Set X
U : Set Y
hKU : (K, U) ∈ S
x : X
hx : x ∈ K
⊢ U ∈ 𝓝 c

Tactic:
exact (hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Topology.CompactOpen
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

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
-- Module: Mathlib.Topology.CompactOpen
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
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
⊢ ∃ (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⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.CompactOpen
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

Tactic:
⟨(⋃ KU ∈ S, KU.1, i), ⟨hSf.isCompact_biUnion <| Prod.forall.2 hScompact, hpi⟩,
      Subset.trans ?_ hSsub⟩

Premises used: Iff.mpr, Set.Subset.trans, Prod.mk, Prod.fst, Set.Finite.isCompact_biUnion, And.intro, Exists.intro, Prod.forall, Set.iUnion
-- Module: Mathlib.Topology.CompactOpen
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
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}
⊢ ∃ (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 ⟨(⋃ KU ∈ S, KU.1, i), ⟨hSf.isCompact_biUnion <| Prod.forall.2 hScompact, hpi⟩,
      Subset.trans ?_ hSsub⟩
-- Module: Mathlib.Topology.CompactOpen
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
refine_1₁ : ∀ (hKne : K.Nonempty), MapsTo (⇑f : (a : X) → Y) K V
⊢ MapsTo (⇑f : (a : X) → Y) K V

Tactic:
rcases K.eq_empty_or_nonempty with rfl | hKne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.CompactOpen
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
V : Set Y
hKV : (∅, V) ∈ S
⊢ MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) ∅ V

Tactic:
mapsTo_empty _ _

Premises used: Set.mapsTo_empty
-- Module: Mathlib.Topology.CompactOpen
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
V : Set Y
hKV : (∅, V) ∈ S
⊢ MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) ∅ V

Tactic:
exact mapsTo_empty _ _

Premises used: Set.mapsTo_empty
-- Module: Mathlib.Topology.CompactOpen
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

Tactic:
hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)

Premises used: Membership.mem.out, Set.subset_biUnion_of_mem, HasSubset.Subset.trans, Set.MapsTo.mono
-- Module: Mathlib.Topology.CompactOpen
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
refine_1 : ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ⊆ V
⊢ MapsTo (⇑f : (a : X) → Y) K V

Tactic:
refine hf.out.mono (subset_biUnion_of_mem (u := Prod.fst) hKV) (hi.trans ?_)

Premises used: Membership.mem.out, Set.subset_biUnion_of_mem, HasSubset.Subset.trans, Set.MapsTo.mono
-- Module: Mathlib.Topology.CompactOpen
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
⊢ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ⊆ V

Tactic:
(biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne

Premises used: HasSubset.Subset.trans, Set.biInter_subset_of_mem, Set.iInter_subset
-- Module: Mathlib.Topology.CompactOpen
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
⊢ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ⊆ V

Tactic:
exact (biInter_subset_of_mem hKV).trans <| iInter_subset _ hKne

Premises used: HasSubset.Subset.trans, Set.biInter_subset_of_mem, Set.iInter_subset
-- Module: Mathlib.Topology.CompactOpen
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
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
⊢ Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) s

Tactic:
rcases hs with ⟨⟨K, i⟩, ⟨hK, hpi⟩, hi⟩
-- Module: Mathlib.Topology.CompactOpen
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
h₁ : ∀ (f : C(X, Y)) (hf : MapsTo (⇑f : (a : X) → Y) K (interior (U i))), f ∈ s
⊢ Membership.mem (γ := Filter C(X, Y)) (𝓝 (const X c)) 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

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, ContinuousMap.eventually_mapsTo
-- Module: Mathlib.Topology.CompactOpen
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
f : C(X, Y)
hf : MapsTo (⇑f : (a : X) → Y) K (interior (U i))
⊢ f ∈ s

Tactic:
hi <| hf.mono_right interior_subset

Premises used: Set.MapsTo.mono_right, interior_subset
-- Module: Mathlib.Topology.CompactOpen
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
f : C(X, Y)
hf : MapsTo (⇑f : (a : X) → Y) K (interior (U i))
⊢ f ∈ s

Tactic:
exact hi <| hf.mono_right interior_subset

Premises used: Set.MapsTo.mono_right, interior_subset
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : C(Y, Z)
⊢ Continuous (X := C(X, Y)) g.comp

Tactic:
continuous_compactOpen.2 fun _K hK _U hU ↦ isOpen_setOf_mapsTo hK (hU.preimage g.2)

Premises used: Iff.mpr, ContinuousMap.isOpen_setOf_mapsTo, ContinuousMap.continuous_compactOpen, ContinuousMap.continuous_toFun, IsOpen.preimage
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : C(Y, Z)
hg : Function.Injective.{u_3 + 1, u_4 + 1} (α := Y) (β := Z) (⇑g : (a : Y) → Z)
⊢ Function.Injective (α := C(X, Y)) g.comp

Tactic:
fun _ _ ↦ (cancel_left hg).1

Premises used: ContinuousMap.cancel_left, Iff.mp, Function.Injective
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : C(Y, Z)
hg : IsInducing.{u_3, u_4} (X := Y) (Y := Z) (⇑g : (a : Y) → Z)
⊢ Eq (α := TopologicalSpace C(X, Y)) compactOpen (induced g.comp compactOpen)

Tactic:
simp only [compactOpen_eq, induced_generateFrom_eq, image_image2, hg.setOf_isOpen,
      image2_image_right, MapsTo, mem_preimage, preimage_setOf_eq, comp_apply]

Premises used: Set.image2_image_right, ContinuousMap.compactOpen_eq, ContinuousMap.comp_apply, Set.image_image2, Set.preimage_setOf_eq, induced_generateFrom_eq, Set.MapsTo, Topology.IsInducing.setOf_isOpen, Set.mem_preimage
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
g : C(Y, Z)
hg : IsEmbedding.{u_3, u_4} (X := Y) (Y := Z) (⇑g : (a : Y) → Z)
⊢ IsEmbedding (X := C(X, Y)) g.comp

Tactic:
⟨isInducing_postcomp g hg.1, postcomp_injective g hg.2⟩

Premises used: ContinuousMap.isInducing_postcomp, Topology.IsEmbedding.injective, ContinuousMap.postcomp_injective, Topology.IsEmbedding.toIsInducing, Topology.IsEmbedding.mk
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen[inst_2] U
⊢ IsOpen (X := C(Y, Z)) {x : C(Y, Z) | MapsTo (⇑(x.comp f) : (a : X) → Z) K U}

Tactic:
simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU

Premises used: ContinuousMap.isOpen_setOf_mapsTo, ContinuousMap.continuous_toFun, Set.mapsTo_image_iff, IsCompact.image
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
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
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : X × C(Y, Z)) ↦ prodMk (const Y p.1) p.2

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt, ContinuousMap.tendsto_nhds_compactOpen]

Premises used: ContinuousAt, ContinuousMap.tendsto_nhds_compactOpen, continuous_iff_continuousAt
-- Module: Mathlib.Topology.CompactOpen
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
⊢ SProd.sprod (α := Set X) (β := Set Z) {r} ((⇑f : (a : Y) → Z) '' K) ⊆ U

Tactic:
simpa [Set.subset_def, forall_comm (α := X)]

Premises used: Set.subset_def, forall_comm
-- Module: Mathlib.Topology.CompactOpen
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
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
⊢ ∀ᶠ (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)])

Premises used: ContinuousMap.continuous, isCompact_singleton, generalized_tube_lemma, IsCompact.image
-- Module: Mathlib.Topology.CompactOpen
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
⊢ r ∈ V

Tactic:
simpa using hrV
-- Module: Mathlib.Topology.CompactOpen
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
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
⊢ ∀ᶠ (a : X × C(Y, Z)) in 𝓝 (r, f), MapsTo (⇑(prodMk (const Y a.1) a.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))) ?_

Premises used: Iff.mpr, prod_mem_nhds, Set.mapsTo_iff_image_subset, Filter.eventually_of_mem, ContinuousMap.eventually_mapsTo, IsOpen.mem_nhds
-- Module: Mathlib.Topology.CompactOpen
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
r' : X
f' : C(Y, Z)
hr'V : (r', f').1 ∈ V
hf' : Membership.mem (γ := Set C(Y, Z)) {x : C(Y, Z) | (fun (g : C(Y, Z)) ↦ MapsTo (⇑g : (a : Y) → Z) K W) x} (r', f').2
x : Y
hxK : x ∈ K
⊢ Membership.mem (α := X × Z) U ((prodMk (const Y (r', f').1) (r', f').2 : (a : Y) → X × Z) x : X × Z)

Tactic:
hVW (Set.mk_mem_prod hr'V (hf' hxK))

Premises used: Set.mk_mem_prod
-- Module: Mathlib.Topology.CompactOpen
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
r' : X
f' : C(Y, Z)
hr'V : (r', f').1 ∈ V
hf' : Membership.mem (γ := Set C(Y, Z)) {x : C(Y, Z) | (fun (g : C(Y, Z)) ↦ MapsTo (⇑g : (a : Y) → Z) K W) x} (r', f').2
x : Y
hxK : x ∈ K
⊢ Membership.mem (α := X × Z) U ((prodMk (const Y (r', f').1) (r', f').2 : (a : Y) → X × Z) x : X × Z)

Tactic:
exact hVW (Set.mk_mem_prod hr'V (hf' hxK))

Premises used: Set.mk_mem_prod