-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst_2 : QuasiCompact iU
inst_3 : QuasiSeparated iU
inst_4 : QuasiCompact iV
inst_5 : QuasiSeparated iV
h₁ :
  CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫
        CategoryStruct.comp (Y := normalization f) (toNormalization f)
          (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (normalizationDesc f
                (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
                  (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
                  (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
                (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
              normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
                (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
              normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f))) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))
h₂ :
  CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫
        CategoryStruct.comp (Y := normalization f) (toNormalization f)
          (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (normalizationDesc f
                (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
                  (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
                  (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
                (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
              normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
            (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
                (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
              normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f))) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))
⊢ Eq (α := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)) ⟶ normalization f)
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫
      CategoryStruct.comp (Y := normalization f) (toNormalization f)
        (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (normalizationDesc f
              (CategoryStruct.comp (Y := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
                (Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))))
                (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f))))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ :
            normalization f ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) :
            normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization f)))
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ toNormalization f ≫ 𝟙 (normalization f))

Tactic:
apply coprod.hom_ext

Premises used: CategoryTheory.Limits.coprod.hom_ext