∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) (h : U ≤ V)
  {Z : AlgebraicGeometry.Scheme} (h_1 : (AlgebraicGeometry.Scheme.IdealSheafData.glueData✝ I).glued ⟶ Z),
  CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h)
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.IdealSheafData.glueData✝¹ I).ι V) h_1) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.IdealSheafData.glueData✝² I).ι U) h_1