∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (x : ↑X.toTopCat),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (IsLocalRing.residue ↑(Y.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f.base) x))))
      (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x)
      (CommRingCat.ofHom (IsLocalRing.residue ↑(X.presheaf.stalk x)))