∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)) {Z : CommRingCat}
  (h :
    { carrier := x.asIdeal.ResidueField,
        commRing := IsLocalRing.instCommRingResidueField (Localization.AtPrime x.asIdeal) } ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).residue x)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.stalkIso R x).hom
      (CategoryTheory.CategoryStruct.comp
        (CommRingCat.ofHom (algebraMap (Localization.AtPrime x.asIdeal) x.asIdeal.ResidueField)) h)