∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Modules.pullback
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y)) =
    AlgebraicGeometry.Scheme.Modules.pullback f