Module: Mathlib.AlgebraicGeometry.Normalization

Goal state before:
pp: case h₁
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inl ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
        toNormalization f ≫
          normalizationDesc f
              ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
                coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
            coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    coprod.inl ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)

pp: case h₂
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inr ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
        toNormalization f ≫
          normalizationDesc f
              ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
                coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
            coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    coprod.inr ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)

Tactic:
<;>

Goal state after:
case h₁
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inl ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
        toNormalization f ≫
          normalizationDesc f
              ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
                coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
            coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    coprod.inl ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)

case h₂
X Y : Scheme
f : X ⟶ Y
inst✝⁵ : QuasiCompact f
inst✝⁴ : QuasiSeparated f
U V : Scheme
iU : U ⟶ X
iV : V ⟶ X
e : IsColimit (BinaryCofan.mk iU iV)
inst✝³ : QuasiCompact iU
inst✝² : QuasiSeparated iU
inst✝¹ : QuasiCompact iV
inst✝ : QuasiSeparated iV
⊢ coprod.inr ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫
        toNormalization f ≫
          normalizationDesc f
              ((e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).hom ≫
                coprod.map (toNormalization (iU ≫ f)) (toNormalization (iV ≫ f)))
              (coprod.desc (fromNormalization (iU ≫ f)) (fromNormalization (iV ≫ f))) ⋯ ≫
            coprod.desc (normalizationDesc (iU ≫ f) (iU ≫ toNormalization f) (fromNormalization f) ⋯)
              (normalizationDesc (iV ≫ f) (iV ≫ toNormalization f) (fromNormalization f) ⋯) =
    coprod.inr ≫
      (e.coconePointUniqueUpToIso (colimit.isColimit (pair U V))).inv ≫ toNormalization f ≫ 𝟙 (normalization f)