∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V),
  CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) (X.restrictStalkIso h x).hom =
    X.presheaf.germ (⋯.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯