∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (i j k : ↑X.affineOpens),
  (AlgebraicGeometry.Scheme.IdealSheafData.glueData✝ I).t' i j k =
    CategoryTheory.Limits.pullback.lift
      (AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux✝ I (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
      (AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux✝¹ I (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯