∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Hom.toImageAux✝ f =
    AlgebraicGeometry.Scheme.Cover.glueMorphisms
      (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f (Y.openCoverOfIsOpenCover (fun i => ↑i) ⋯))
      (fun U =>
        CategoryTheory.CategoryStruct.comp
          (AlgebraicGeometry.Scheme.Hom.liftQuotient
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (↑U).ι) (↑U).toSpecΓ)
            ((AlgebraicGeometry.Scheme.Hom.ker f).ideal U) ⋯)
          ((AlgebraicGeometry.Scheme.Hom.ker f).subschemeCover.f U))
      ⋯