awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
h : ∀ (f : X → Prop), (∀ s ∈ S, ContinuousOn f s) → Continuous[inst, _] f
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u)
⊢ ∀ (f : X → Prop),
    (∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] {x : (↑s : Type u_1) | s.restrict (π := fun (a : X) ↦ Prop) f x}) →
      IsOpen[inst] {x : X | f x}

Tactic:
simp only [continuousOn_iff_continuous_restrict, continuous_Prop] at *

Premises used: continuousOn_iff_continuous_restrict, continuous_Prop
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u)
h :
  ∀ (f : X → Prop),
    (∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] {x : (↑s : Type u_1) | s.restrict (π := fun (a : X) ↦ Prop) f x}) →
      IsOpen[inst] {x : X | f x}
⊢ IsOpen[inst] u

Tactic:
h _ hu

Premises used: setOf
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
u : Set X
hu : ∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' u)
h :
  ∀ (f : X → Prop),
    (∀ s ∈ S, IsOpen[instTopologicalSpaceSubtype] {x : (↑s : Type u_1) | s.restrict (π := fun (a : X) ↦ Prop) f x}) →
      IsOpen[inst] {x : X | f x}
⊢ IsOpen[inst] u

Tactic:
exact h _ hu
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
h :
  ∀ (t : Set X),
    (∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)) → IsClosed[inst] t
⊢ IsCoherentWith S

Tactic:
⟨fun _t ht ↦ isClosed_compl_iff.1 <| h _ fun s hs ↦ (ht s hs).isClosed_compl⟩

Premises used: Compl.compl, IsOpen.isClosed_compl, Topology.IsCoherentWith.mk, Iff.mp, isClosed_compl_iff
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set (Set X)
hS : IsCoherentWith S
hT : ∀ s ∈ S, ∃ t ∈ T, s ⊆ t
⊢ IsCoherentWith T

Tactic:
of_continuous_prop fun _f hf ↦ hS.continuous_iff.2 fun s hs ↦
    let ⟨t, htT, hst⟩ := hT s hs; (hf t htT).mono hst

Premises used: Iff.mpr, Topology.IsCoherentWith.of_continuous_prop, Topology.IsCoherentWith.continuous_iff, ContinuousOn.mono, ContinuousOn, _private.0.Topology.IsCoherentWith.enlarge.match_1
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S T : Set (Set X)
hS : IsCoherentWith S
hT : S ⊆ T
⊢ IsCoherentWith T

Tactic:
hS.enlarge fun s hs ↦ ⟨s, hT hs, Subset.rfl⟩

Premises used: Topology.IsCoherentWith.enlarge, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
⊢ IsCoherentWith S

Tactic:
of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_

Premises used: Topology.IsCoherentWith.of_isClosed, IsSeqClosed.isClosed
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
refine :
  ∀ (t : Set X) (ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t))
    (u : ℕ → X) (x : X) (hut : ∀ (n : ℕ), u n ∈ t) (hux : Tendsto u atTop (𝓝 x)), x ∈ t
⊢ IsCoherentWith S

Tactic:
refine of_isClosed fun t ht ↦ IsSeqClosed.isClosed fun u x hut hux ↦ ?_

Premises used: Topology.IsCoherentWith.of_isClosed, IsSeqClosed.isClosed
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
rcases :
  ∀ (s : Set X) (hsc : IsClosed[inst] s)
    (hst :
      Eq (α := Set (↑(insert x (range u)) : Type u_1))
        (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' s)
        (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' t)),
    x ∈ t
⊢ x ∈ t

Tactic:
rcases isClosed_induced_iff.1 (ht _ (h hux)) with ⟨s, hsc, hst⟩

Premises used: isClosed_induced_iff, Iff.mp
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst :
  Eq (α := Set (↑(insert x (range u)) : Type u_1)) (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' s)
    (Subtype.val (p := fun (x_1 : X) ↦ x_1 ∈ insert x (range u)) ⁻¹' t)
⊢ ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t

Tactic:
rw [Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff] at hst

Premises used: Subtype.preimage_val_eq_preimage_val_iff, Set.ext_iff
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
this : x ∈ s
⊢ x ∈ insert x (range u) ∩ s ↔ x ∈ insert x (range u) ∩ t

Tactic:
specialize hst x
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
this : x ∈ s
hst : x ∈ insert x (range u) ∩ s ↔ x ∈ insert x (range u) ∩ t
⊢ x ∈ t

Tactic:
simp_all
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
suffices : x ∈ s
⊢ x ∈ t

Tactic:
suffices x ∈ s by specialize hst x; simp_all
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
⊢ x ∈ s

Tactic:
hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
refine : ∀ (k : ℕ), u k ∈ s
⊢ x ∈ s

Tactic:
refine hsc.mem_of_tendsto hux <| Eventually.of_forall fun k ↦ ?_

Premises used: IsClosed.mem_of_tendsto, Filter.Eventually.of_forall
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
hst : ∀ (x_1 : X), x_1 ∈ insert x (range u) ∩ s ↔ x_1 ∈ insert x (range u) ∩ t
k : ℕ
⊢ u k ∈ insert x (range u) ∩ s ↔ u k ∈ insert x (range u) ∩ t

Tactic:
specialize hst (u k)
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
inst_1 : SequentialSpace X
h : ∀ ⦃u : ℕ → X⦄ ⦃x : X⦄, Tendsto u atTop (𝓝 x) → insert x (range u) ∈ S
t : Set X
ht : ∀ s ∈ S, IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' t)
u : ℕ → X
x : X
hut : ∀ (n : ℕ), u n ∈ t
hux : Tendsto u atTop (𝓝 x)
s : Set X
hsc : IsClosed[inst] s
k : ℕ
hst : u k ∈ insert x (range u) ∩ s ↔ u k ∈ insert x (range u) ∩ t
⊢ u k ∈ s

Tactic:
simp_all
-- Module: Mathlib.Topology.Coherent
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Set (Set X)
h : ∀ (x : X), ∃ s ∈ S, s ∈ 𝓝 x
⊢ IsCoherentWith S

Tactic:
of_continuous_prop fun _f hf ↦ continuous_iff_continuousAt.2 fun x ↦
    let ⟨s, hsS, hsx⟩ := h x
    (hf s hsS).continuousAt hsx

Premises used: Iff.mpr, Topology.IsCoherentWith.of_continuous_prop, _private.0.Topology.IsCoherentWith.of_nhds.match_1, ContinuousAt, ContinuousOn.continuousAt, continuous_iff_continuousAt
-- 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
    (generateFrom
      (image2 (fun (K : Set X) (U : Set Y) ↦ {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}) {K : Set X | IsCompact K}
        {t : Set Y | IsOpen[inst_1] t}))

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
K : Set X
U : Set Y
hK : IsCompact K
hU : IsOpen[inst_1] U
⊢ IsOpen (X := C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}

Tactic:
isOpen_generateFrom_of_mem <| mem_image2_of_mem hK hU

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem, Set.mem_image2_of_mem
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
K : Set X
U : Set Y
f : C(X, Y)
hK : IsCompact K
hU : IsOpen[inst_1] U
h : MapsTo (⇑f : (a : X) → Y) K U
⊢ ∀ᶠ (g : C(X, Y)) in 𝓝 f, MapsTo (⇑g : (a : X) → Y) K U

Tactic:
(isOpen_setOf_mapsTo hK hU).mem_nhds h

Premises used: ContinuousMap.isOpen_setOf_mapsTo, Set.Mem, Filter.Eventually, setOf, IsOpen.mem_nhds
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set Y
inst_2 : CompactSpace X
hU : IsOpen[inst_1] U
simp_rw : IsOpen (X := C(X, Y)) {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) univ U}
⊢ IsOpen (X := C(X, Y)) {f : C(X, Y) | range.{u_3, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ U}

Tactic:
simp_rw [← mapsTo_univ_iff_range_subset]

Premises used: Set.mapsTo_univ_iff_range_subset
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set Y
inst_2 : CompactSpace X
hU : IsOpen[inst_1] U
⊢ IsOpen (X := C(X, Y)) {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) univ U}

Tactic:
isOpen_setOf_mapsTo isCompact_univ hU

Premises used: ContinuousMap.isOpen_setOf_mapsTo, isCompact_univ
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set Y
inst_2 : CompactSpace X
hU : IsOpen[inst_1] U
⊢ IsOpen (X := C(X, Y)) {f : C(X, Y) | MapsTo.{u_2, u_3} (α := X) (⇑f : (a : X) → Y) univ U}

Tactic:
exact isOpen_setOf_mapsTo isCompact_univ hU

Premises used: ContinuousMap.isOpen_setOf_mapsTo, isCompact_univ
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
U : Set Y
inst_2 : CompactSpace X
f : C(X, Y)
hU : IsOpen[inst_1] U
h : range.{u_3, u_2 + 1} (ι := X) (⇑f : (a : X) → Y) ⊆ U
⊢ ∀ᶠ (g : C(X, Y)) in 𝓝 f, range.{u_3, u_2 + 1} (ι := X) (⇑g : (a : X) → Y) ⊆ U

Tactic:
(isOpen_setOf_range_subset hU).mem_nhds h

Premises used: Set.Mem, Filter.Eventually, setOf, IsOpen.mem_nhds, ContinuousMap.isOpen_setOf_range_subset
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace Y
inst_1 : TopologicalSpace Z
l : Filter α
f : α → C(Y, Z)
g : C(Y, Z)
⊢ Tendsto f l (𝓝 g) ↔
    ∀ (K : Set Y),
      IsCompact K →
        ∀ (U : Set Z),
          IsOpen[inst_1] U → MapsTo (⇑g : (a : Y) → Z) K U → ∀ᶠ (a : α) in l, MapsTo (⇑(f a) : (a : Y) → Z) K U

Tactic:
simp [nhds_compactOpen]

Premises used: ContinuousMap.nhds_compactOpen
-- 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 : X → C(Y, Z)
⊢ Continuous[inst, _] f ↔
    ∀ (K : Set Y),
      IsCompact K → ∀ (U : Set Z), IsOpen[inst_2] U → IsOpen[inst] {x : X | MapsTo (⇑(f x) : (a : Y) → Z) K U}

Tactic:
continuous_generateFrom_iff.trans forall_mem_image2

Premises used: Set.forall_mem_image2, Iff.trans, continuous_generateFrom_iff
-- 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).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}

Tactic:
⟨fun s ↦ ?_⟩

Premises used: Filter.HasBasis.mk
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : C(X, Y)
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
⊢ (𝓝 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}

Tactic:
refine ⟨fun s ↦ ?_⟩
-- Module: Mathlib.Topology.CompactOpen
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)
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
⊢ 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:
simp_rw [nhds_compactOpen, iInf_comm.{_, 0, _ + 1}, iInf_prod', iInf_and']

Premises used: iInf_prod', iInf_and', iInf_comm, ContinuousMap.nhds_compactOpen
-- Module: Mathlib.Topology.CompactOpen
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)
⊢ 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 [mem_biInf_principal, and_assoc]

Premises used: Filter.mem_biInf_principal, and_assoc
-- Module: Mathlib.Topology.CompactOpen
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 ↔
    ∃ (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) ∧
          {g : C(X, Y) | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → MapsTo (⇑g : (a : X) → Y) K U} ⊆ s

Tactic:
simp [f.hasBasis_nhds.mem_iff, ← setOf_forall, and_assoc]

Premises used: ContinuousMap.hasBasis_nhds, Filter.HasBasis.mem_iff, and_assoc, Set.setOf_forall
-- 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
⊢ 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)}

Tactic:
⟨fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩⟩

Premises used: Filter.HasBasis.mk, Iff.intro
-- 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
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
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
⊢ 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)}

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun hs ↦ ?_⟩⟩
-- 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
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
⊢ ∃ (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⟩

Premises used: ContinuousMap.mem_nhds_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
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
⊢ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K

Tactic:
choose hScompact hSopen hSmaps using hS
-- 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
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
⊢ ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsOpen[inst_1] U

Tactic:
choose hScompact hSopen hSmaps using hS
-- 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
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
⊢ ∀ (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
-- 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
simp : ∀ (a : Set X) (b : Set Y), (a, b) ∈ S → ∀ (i : a.Nonempty), b ∈ 𝓝 c
⊢ ⋂ KU ∈ S, ⋂ (_ : KU.1.Nonempty), KU.2 ∈ 𝓝 c

Tactic:
simp only [biInter_mem hSf, Prod.forall, iInter_mem]

Premises used: Filter.iInter_mem, Filter.biInter_mem, Prod.forall
-- 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:
(hSopen K U hKU).mem_nhds <| hSmaps K U hKU hx

Premises used: IsOpen.mem_nhds