∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.inv (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp hU.fromSpec h