∀ {X Y : TopCat} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑X)
  (H : IsOpen (⇑(CategoryTheory.ConcreteCategory.hom f) '' ↑U))
  (s :
    CategoryTheory.Limits.Cone
      (CategoryTheory.Functor.empty
        (CategoryTheory.CostructuredArrow (TopologicalSpace.Opens.map f).op (Opposite.op U)))),
  autoParam
    (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f).op.map (id (CategoryTheory.homOfLE ⋯).op))
        (CategoryTheory.Limits.asEmptyCone (CategoryTheory.CostructuredArrow.mk (CategoryTheory.homOfLE ⋯).op)).pt.hom =
      s.pt.hom)
    CategoryTheory.CostructuredArrow.homMk._auto_1