{X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.IsOpenImmersion f] →
      (x : ↥X) →
        (AlgebraicGeometry.Scheme.Modules.restrictFunctor f).comp
            ((AlgebraicGeometry.Scheme.Modules.toPresheaf X).comp (TopCat.Presheaf.stalkFunctor Ab x)) ≅
          (AlgebraicGeometry.Scheme.Modules.toPresheaf Y).comp (TopCat.Presheaf.stalkFunctor Ab (f x))