∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (x : ↥X),
  CategoryTheory.CategoryStruct.comp (Y.Γevaluation (f x)) (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop f) (X.Γevaluation x)