∀ {X : AlgebraicGeometry.Scheme} {M : X.Modules} {U : X.Opens},
  AlgebraicGeometry.Scheme.Modules.Hom.app (AlgebraicGeometry.Scheme.Modules.restrictFunctorId.inv.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op