∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (ij : ↑X.affineOpens × ↑X.affineOpens),
  (AlgebraicGeometry.Scheme.IdealSheafData.glueData✝ I).V ij =
    AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjPullback✝ I ij.1 ij.2