∀ (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U),
  CategoryTheory.Limits.HasColimit
    (((CategoryTheory.Functor.whiskeringLeft (TopologicalSpace.OpenNhds ↑x)ᵒᵖ
              (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ CommRingCat).obj
          (TopologicalSpace.OpenNhds.inclusion ↑x).op).obj
      X.presheaf)