∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat) {Z : CommRingCat}
  (h : Y.presheaf.stalk y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom ((CategoryTheory.ConcreteCategory.hom e.inv.base) y))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯) h