∀ {U : TopCat} (X : AlgebraicGeometry.Scheme) {f : U ⟶ TopCat.of ↥X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (X_1 : (TopologicalSpace.Opens ↑U)ᵒᵖ),
  (X.restrict h).presheaf.obj X_1 = X.presheaf.obj (Opposite.op (h.functor.obj (Opposite.unop X_1)))