∀ (Y : AlgebraicGeometry.Scheme) {I J : Y.IdealSheafDataᵒᵖ} (h : I ⟶ J),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯)
      (CategoryTheory.Over.mk (Opposite.unop J).subschemeι).hom =
    (CategoryTheory.Over.mk (Opposite.unop I).subschemeι).hom