awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : LocallyCompactPair Y Z
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
⊢ Continuous (Y := C(X, Z)) fun (x : C(X, Y) × C(Y, Z)) ↦ x.2.comp x.1

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt, 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
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 :
  ∀ (hKU : Set.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), Set.MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U
⊢ Set.MapsTo (⇑((f, g).2.comp (f, g).1) : (a : X) → Z) K U →
    ∀ᶠ (a : C(X, Y) × C(Y, Z)) in 𝓝 (f, g), Set.MapsTo (⇑(a.2.comp a.1) : (a : X) → Z) K U

Tactic:
(hKU : MapsTo (g ∘ f) K U)
-- 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
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),
    Membership.mem (γ := Filter Y) (𝓝ˢ ((⇑f : (a : X) → Y) '' K)) L ∧ IsCompact L ∧ MapsTo (⇑g : (a : Y) → Z) L U

Tactic:
exists_mem_nhdsSet_isCompact_mapsTo g.continuous (hK.image f.continuous) hU
      (mapsTo_image_iff.2 hKU)

Premises used: Iff.mpr, ContinuousMap.continuous, exists_mem_nhdsSet_isCompact_mapsTo, 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
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
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
⊢ ∀ᶠ (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)

Premises used: Iff.mpr, ContinuousMap.continuous, exists_mem_nhdsSet_isCompact_mapsTo, Set.mapsTo_image_iff, Set.image, nhdsSet, IsCompact.image, DFunLike.coe
-- 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
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
⊢ MapsTo (⇑f : (a : X) → Y) K (interior L)

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL

Premises used: Set.mapsTo_iff_image_subset, subset_interior_iff_mem_nhdsSet
-- 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
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
hKL₁ : MapsTo (⇑f : (a : X) → Y) K (interior L)
⊢ IsCompact L

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL

Premises used: Set.mapsTo_iff_image_subset, subset_interior_iff_mem_nhdsSet
-- 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
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
hKL₁ : MapsTo (⇑f : (a : X) → Y) K (interior L)
hLc₁ : IsCompact L
⊢ MapsTo (⇑g : (a : Y) → Z) L U

Tactic:
rw [← subset_interior_iff_mem_nhdsSet, ← mapsTo_iff_image_subset] at hKL

Premises used: Set.mapsTo_iff_image_subset, subset_interior_iff_mem_nhdsSet
-- 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
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 : MapsTo (⇑f : (a : X) → Y) K (interior 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:
((eventually_mapsTo hK isOpen_interior hKL).prod_nhds
    (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
      hg'.comp <| hf'.mono_right interior_subset

Premises used: Set.MapsTo.mono_right, interior_subset, isOpen_interior, ContinuousMap.comp, Prod.mk, Prod.fst, _private.0.ContinuousMap.continuous_comp'.match_2, Filter.Eventually.mono, ContinuousMap.eventually_mapsTo, Set.MapsTo.comp, Set.MapsTo, _private.0.ContinuousMap.continuous_comp'.match_3, Filter.Eventually.prod_nhds, Prod.snd, DFunLike.coe
-- 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
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 : MapsTo (⇑f : (a : X) → Y) K (interior 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:
exact ((eventually_mapsTo hK isOpen_interior hKL).prod_nhds
    (eventually_mapsTo hLc hU hLU)).mono fun ⟨f', g'⟩ ⟨hf', hg'⟩ ↦
      hg'.comp <| hf'.mono_right interior_subset

Premises used: isOpen_interior, Filter.Eventually.mono, ContinuousMap.eventually_mapsTo, Filter.Eventually.prod_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
inst_3 : LocallyCompactPair Y Z
α : Type u_6
l : Filter α
g : α → C(Y, Z)
g₀ : C(Y, Z)
f : α → C(X, Y)
f₀ : C(X, Y)
hg : Tendsto g l (𝓝 g₀)
hf : Tendsto f l (𝓝 f₀)
⊢ Tendsto (fun (a : α) ↦ (g a).comp (f a)) l (𝓝 (g₀.comp f₀))

Tactic:
(continuous_comp'.tendsto (f₀, g₀)).comp (hf.prodMk_nhds hg)

Premises used: ContinuousMap.comp, Prod.mk, Continuous.tendsto, ContinuousMap.continuous_comp', Filter.Tendsto.comp, Filter.Tendsto.prodMk_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
inst_3 : LocallyCompactPair Y Z
X' : Type u_6
inst_4 : TopologicalSpace X'
a : X'
g : X' → C(Y, Z)
f : X' → C(X, Y)
hg : ContinuousAt g a
hf : ContinuousAt f a
⊢ ContinuousAt (Y := C(X, Z)) (fun (x : X') ↦ (g x).comp (f x)) a

Tactic:
hg.compCM hf

Premises used: ContinuousAt, Filter.Tendsto.compCM
-- 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
inst_3 : LocallyCompactPair Y Z
X' : Type u_6
inst_4 : TopologicalSpace X'
a : X'
g : X' → C(Y, Z)
f : X' → C(X, Y)
s : Set X'
hg : ContinuousWithinAt g s a
hf : ContinuousWithinAt f s a
⊢ ContinuousWithinAt (Y := C(X, Z)) (fun (x : X') ↦ (g x).comp (f x)) s a

Tactic:
hg.compCM hf

Premises used: ContinuousWithinAt, Filter.Tendsto.compCM
-- 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
inst_3 : LocallyCompactPair Y Z
X' : Type u_6
inst_4 : TopologicalSpace X'
g : X' → C(Y, Z)
f : X' → C(X, Y)
s : Set X'
hg : ContinuousOn g s
hf : ContinuousOn f s
⊢ ContinuousOn (Y := C(X, Z)) (fun (x : X') ↦ (g x).comp (f x)) s

Tactic:
fun a ha ↦
  (hg a ha).compCM (hf a ha)

Premises used: ContinuousWithinAt.compCM, ContinuousOn
-- 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
inst_3 : LocallyCompactPair Y Z
X' : Type u_6
inst_4 : TopologicalSpace X'
g : X' → C(Y, Z)
f : X' → C(X, Y)
hg : Continuous[inst_4, _] g
hf : Continuous[inst_4, _] f
⊢ Continuous[inst_4, _] fun (x : X') ↦ (g x).comp (f x)

Tactic:
continuous_comp'.comp (hf.prodMk hg)

Premises used: Continuous.comp, ContinuousMap.comp, ContinuousMap.continuous_comp', Continuous.prodMk
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : LocallyCompactPair X Y
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)
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (fx : C(X, Y) × X) ↦ (fx.1 : (a : X) → Y) fx.2

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt, (nhds_basis_opens _).tendsto_right_iff]

Premises used: ContinuousAt, Filter.HasBasis.tendsto_right_iff, nhds_basis_opens, continuous_iff_continuousAt
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U_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
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)
⊢ ∀ᶠ (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⟩

Premises used: ContinuousMap.continuous, LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo, IsOpen.mem_nhds
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : 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
⊢ ∀ 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:
fun _ h ↦ h.1 h.2

Premises used: Set.Mem, And.right, And.left
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : 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
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)
⊢ ∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), Membership.mem (α := Y) U ((x.1 : (a : X) → Y) x.2 : Y)

Tactic:
filter_upwards [prod_mem_nhds (eventually_mapsTo hK hU hKU) hxK] using fun _ h ↦ h.1 h.2

Premises used: prod_mem_nhds, ContinuousMap.eventually_mapsTo
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U_1 : Set Y
x : X
U : Set Y
hU : IsOpen[inst_1] U
⊢ IsOpen (X := C(X, Y)) ((fun (f : C(X, Y)) ↦ (f : (a : X) → Y) x) ⁻¹' U)

Tactic:
simpa using isOpen_setOf_mapsTo isCompact_singleton hU

Premises used: ContinuousMap.isOpen_setOf_mapsTo, isCompact_singleton
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
t : Set Y
ht : IsClosed[inst_1] t
s : Set X
⊢ IsClosed (X := C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) s t}

Tactic:
ht.setOf_mapsTo fun _ _ ↦ continuous_eval_const _

Premises used: ContinuousEvalConst.continuous_eval_const, IsClosed.setOf_mapsTo
-- 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 : IsClopen U
⊢ IsClopen (X := C(X, Y)) {f : C(X, Y) | MapsTo (⇑f : (a : X) → Y) K U}

Tactic:
⟨isClosed_setOf_mapsTo hU.isClosed K, isOpen_setOf_mapsTo hK hU.isOpen⟩

Premises used: ContinuousMap.isOpen_setOf_mapsTo, IsClopen.isOpen, IsClopen.isClosed, And.intro, ContinuousMap.isClosed_setOf_mapsTo, IsClopen
-- Module: Mathlib.Topology.CompactOpen
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ h.map continuous_coeFun⟩

Premises used: Iff.intro, continuous_coeFun, Specializes.map
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
refine : ∀ (h : Specializes (X := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y)), f ⤳ g
⊢ 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⟩
-- Module: Mathlib.Topology.CompactOpen
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)
this :
  ∀ (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
⊢ f ⤳ g

Tactic:
simpa [specializes_iff_pure, nhds_compactOpen]

Premises used: specializes_iff_pure, ContinuousMap.nhds_compactOpen
-- Module: Mathlib.Topology.CompactOpen
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)
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
⊢ f ⤳ g

Tactic:
suffices ∀ K, IsCompact K → ∀ U, IsOpen U → MapsTo g K U → MapsTo f K U by
    simpa [specializes_iff_pure, nhds_compactOpen]
-- Module: Mathlib.Topology.CompactOpen
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)
⊢ ∀ (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:
fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)

Premises used: Specializes.mem_open, Set.MapsTo, continuous_apply, Specializes.map
-- Module: Mathlib.Topology.CompactOpen
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)
⊢ ∀ (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:
exact fun K _ U hU hg x hx ↦ (h.map (continuous_apply x)).mem_open hU (hg hx)

Premises used: Specializes.mem_open, continuous_apply, Specializes.map
-- Module: Mathlib.Topology.CompactOpen
Goal:
X : Type u_2
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f g : C(X, Y)
⊢ Inseparable (X := (a : X) → Y) (⇑f : (a : X) → Y) (⇑g : (a : X) → Y) ↔ Inseparable f g

Tactic:
simp only [inseparable_iff_specializes_and, specializes_coe]

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

Tactic:
t0Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun

Premises used: t0Space_of_injective_of_continuous, DFunLike.coe_injective, continuous_coeFun
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : R0Space Y
f g : C(X, Y)
h : f ⤳ g
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)
⊢ g ⤳ f

Tactic:
rw [← specializes_coe] at h ⊢

Premises used: ContinuousMap.specializes_coe
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : R0Space Y
f g : C(X, Y)
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:
h.symm

Premises used: Specializes.symm
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : R0Space Y
f g : C(X, Y)
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:
exact h.symm

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

Tactic:
t1Space_of_injective_of_continuous DFunLike.coe_injective continuous_coeFun

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

Tactic:
.of_continuous_specializes_imp continuous_coeFun fun _ _ ↦ specializes_coe.1

Premises used: ContinuousMap.specializes_coe, R1Space.of_continuous_specializes_imp, Iff.mp, continuous_coeFun
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : T2Space Y
⊢ T2Space C(X, Y)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K : Set X
U : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
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
⊢ (𝓝 f).lift' closure ≤ 𝓝 f

Tactic:
rw [← tendsto_id', tendsto_nhds_compactOpen]

Premises used: Filter.tendsto_id', ContinuousMap.tendsto_nhds_compactOpen
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hf : MapsTo (⇑f : (a : X) → Y) K U
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
⊢ ∀ᶠ (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⟩

Premises used: Iff.mpr, ContinuousMap.continuous, IsCompact.exists_isOpen_closure_subset, IsCompact.image, Set.MapsTo.image_subset, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.CompactOpen
Goal:
α : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
T : Type u_5
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : TopologicalSpace Z
inst_3 : TopologicalSpace T
K_1 : Set X
U_1 : Set Y
inst_4 : RegularSpace Y
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst_1] U
hf : MapsTo (⇑f : (a : X) → Y) K U
V : Set Y
hVo : IsOpen[inst_1] V
hKV : (⇑f : (a : X) → Y) '' K ⊆ V
hVU : closure[inst_1] V ⊆ U
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
⊢ ∀ᶠ (a : C(X, Y)) in (𝓝 f).lift' closure, MapsTo (⇑(id a) : (a : X) → Y) K U

Tactic:
filter_upwards [mem_lift' (eventually_mapsTo hK hVo (mapsTo_iff_image_subset.2 hKV))] with g hg

Premises used: Iff.mpr, Set.mapsTo_iff_image_subset, Filter.mem_lift', ContinuousMap.eventually_mapsTo