∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc
        (AlgebraicGeometry.Scheme.Hom.normalizationDesc (CategoryTheory.CategoryStruct.comp iU f)
          (CategoryTheory.CategoryStruct.comp iU (AlgebraicGeometry.Scheme.Hom.toNormalization f))
          (AlgebraicGeometry.Scheme.Hom.fromNormalization f) ⋯)
        (AlgebraicGeometry.Scheme.Hom.normalizationDesc (CategoryTheory.CategoryStruct.comp iV f)
          (CategoryTheory.CategoryStruct.comp iV (AlgebraicGeometry.Scheme.Hom.toNormalization f))
          (AlgebraicGeometry.Scheme.Hom.fromNormalization f) ⋯))
      (AlgebraicGeometry.Scheme.Hom.normalizationDesc f
        (CategoryTheory.CategoryStruct.comp
          (e.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.pair U V))).hom
          (CategoryTheory.Limits.coprod.map
            (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iU f))
            (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))))
        (CategoryTheory.Limits.coprod.desc
          (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iU f))
          (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iV f)))
        ⋯) =
    CategoryTheory.CategoryStruct.id
      (AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿
        AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iV f))