awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))) ≫ f) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
h₂ :
  CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))
⊢ Eq (α := Cocone.pt (F := pair U V) (colimit.cocone (pair U V)) ⟶ Y)
    (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))

Tactic:
apply coprod.hom_ext

Premises used: CategoryTheory.Limits.coprod.hom_ext
-- 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
⊢ CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inl
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))

Tactic:
simp
-- 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
⊢ CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (Iso.inv (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))) ≫ f) =
    CategoryStruct.comp (Y := U ⨿ V) coprod.inr
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
        (coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
        (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))))

Tactic:
simp
-- 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 := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯)) =
    coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
h₂ :
  CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯)) =
    coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
⊢ Eq (α := normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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 (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
    (𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) :
      normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
ext
-- 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
⊢ Eq (α := normalization (iU ≫ f) ⟶ Y)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
          (CategoryStruct.comp (Y := normalization f)
            (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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 (iU ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) :
        normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ Y))
    (fromNormalization (iU ≫ f))

Tactic:
simp
-- 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
⊢ (coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization (iU ≫ f)

Tactic:
simp
-- 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 := normalization (iU ≫ f)) (toNormalization (iU ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
        (CategoryStruct.comp (Y := normalization f)
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯))) =
    toNormalization (iU ≫ f) ≫ coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
⊢ CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯)) =
    coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
refine Scheme.Hom.normalization.hom_ext _ _ _
        (coprod.desc (iU ≫ f).fromNormalization (iV ≫ f).fromNormalization) ?_ (by simp) (by simp)

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, CategoryTheory.Limits.coprod.desc, AlgebraicGeometry.Scheme.Hom.normalization.hom_ext, CategoryTheory.CategoryStruct.comp
-- 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
⊢ Eq (α := U ⟶ Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
    (iU ≫ Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V)))) coprod.inl

Tactic:
have H : iU ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inl :=
        e.comp_coconePointUniqueUpToIso_hom (colimit.isColimit (pair U V)) ⟨.left⟩
-- 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 :
  Eq (α := U ⟶ Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
    (iU ≫ Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V)))) coprod.inl
⊢ CategoryStruct.comp (Y := normalization (iU ≫ f)) (toNormalization (iU ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inl
        (CategoryStruct.comp (Y := normalization f)
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯))) =
    toNormalization (iU ≫ f) ≫ coprod.inl ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
simp [reassoc_of% H]
-- 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
⊢ Eq (α := normalization (iV ≫ f) ⟶ Y)
    (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
          (CategoryStruct.comp (Y := normalization f)
            (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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 (iV ≫ f) ⟶ normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
      (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) :
        normalization (iU ≫ f) ⨿ normalization (iV ≫ f) ⟶ Y))
    (fromNormalization (iV ≫ f))

Tactic:
simp
-- 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
⊢ (coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))) ≫
      coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f)) =
    fromNormalization (iV ≫ f)

Tactic:
simp
-- 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 := normalization (iV ≫ f)) (toNormalization (iV ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
        (CategoryStruct.comp (Y := normalization f)
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯))) =
    toNormalization (iV ≫ f) ≫ coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))
⊢ CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
      (CategoryStruct.comp (Y := normalization f)
        (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
          (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯)) =
    coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
refine Scheme.Hom.normalization.hom_ext _ _ _
        (coprod.desc (iU ≫ f).fromNormalization (iV ≫ f).fromNormalization) ?_ (by simp) (by simp)

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, CategoryTheory.Limits.coprod.desc, AlgebraicGeometry.Scheme.Hom.normalization.hom_ext, CategoryTheory.CategoryStruct.comp
-- 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
⊢ Eq (α := V ⟶ Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
    (iV ≫ Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V)))) coprod.inr

Tactic:
have H : iV ≫ (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom = coprod.inr :=
        e.comp_coconePointUniqueUpToIso_hom (colimit.isColimit (pair U V)) ⟨.right⟩
-- 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 :
  Eq (α := V ⟶ Cocone.pt (F := pair U V) (colimit.cocone (pair U V)))
    (iV ≫ Iso.hom (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V)))) coprod.inr
⊢ CategoryStruct.comp (Y := normalization (iV ≫ f)) (toNormalization (iV ≫ f))
      (CategoryStruct.comp (Y := normalization (iU ≫ f) ⨿ normalization (iV ≫ f)) coprod.inr
        (CategoryStruct.comp (Y := normalization f)
          (coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
            (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization 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))) ⋯))) =
    toNormalization (iV ≫ f) ≫ coprod.inr ≫ 𝟙 (normalization (iU ≫ f) ⨿ normalization (iV ≫ f))

Tactic:
simp [reassoc_of% H]
-- 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
⊢ Eq (α := normalization f ⟶ Y)
    (CategoryStruct.comp (Y := normalization 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))
      (fromNormalization f))
    (fromNormalization f)

Tactic:
simp
-- 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
⊢ 𝟙 (normalization f) ≫ fromNormalization f = fromNormalization f

Tactic:
simp
-- 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
refine :
  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)) =
    toNormalization f ≫ 𝟙 (normalization 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) =
    𝟙 (normalization f)

Tactic:
refine Scheme.Hom.normalization.hom_ext _ _ _ f.fromNormalization ?_ (by simp) (by simp)

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, AlgebraicGeometry.Scheme.Hom.normalization.hom_ext