∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData),
  I.subschemeCover =
    { I₀ := ↑X.affineOpens,
      X := fun U =>
        { carrier := ↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U, commRing := Ideal.Quotient.commRing (I.ideal U) },
      f := fun U =>
        CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.IdealSheafData.glueData✝ I).ι U)
          (AlgebraicGeometry.Scheme.IdealSheafData.subschemeIso✝ I).inv,
      idx := fun x => AlgebraicGeometry.Scheme.Cover.idx (X.openCoverOfIsOpenCover (fun i => ↑i) ⋯) ↑x, covers := ⋯,
      map_prop := ⋯ }