-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : QuasiCompact f_1
inst_1 : QuasiSeparated f_1
X S Y : Scheme
f : X ⟶ S
g : Y ⟶ S
inst_2 : QuasiCompact f
inst_3 : QuasiSeparated f
inst_4 : Smooth g
x : ↥(pullback (X := normalization f) (fromNormalization f) g)
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) ((pullback.snd (fromNormalization f) g ≫ g) x : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x : ↥Y)
hVU : V ≤ g ⁻¹ᵁ U
W : (pullback (X := normalization f) (fromNormalization f) g).Opens := pullback.snd (fromNormalization f) g ⁻¹ᵁ V
this_1 :
  IsIso (X :=
    pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U))
      (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU))
    (Y := Γ(pullback (fromNormalization f) g, W)) (pushoutSection ⋯ hVU ⋯ ⋯)
this_2 : (CommRingCat.Hom.hom (appLE g U V hVU)).Smooth
algInst : Algebra (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
algInst_1 : Algebra (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) := (CommRingCat.Hom.hom (appLE g U V hVU)).toAlgebra
algInst_2 : Algebra (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app (pullback.snd f g) V))
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u)
this : IsIso (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (pushoutSection ⋯ hVU ⋯ ⋯)
e₀ : CommRingCat.of
    ((↑(Y.presheaf.1 (Opposite.op V)) : Type u) ⊗[(↑(S.presheaf.1 (Opposite.op U)) : Type u)]
      (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)) ≅
  Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) :=
  Iso.trans (Y :=
    pushout (X := CommRingCat.of (↑(S.presheaf.1 (Opposite.op U)) : Type u)) (Y :=
      CommRingCat.of (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)) (Z :=
      CommRingCat.of (↑(Y.presheaf.1 (Opposite.op V)) : Type u))
      (CommRingCat.ofHom
        (algebraMap (↑(S.presheaf.1 (Opposite.op U)) : Type u) (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)))
      (CommRingCat.ofHom
        (algebraMap (↑(S.presheaf.1 (Opposite.op U)) : Type u) (↑(Y.presheaf.1 (Opposite.op V)) : Type u))))
    (IsPushout.isoPushout ⋯) (pushout.congrHom ⋯ ⋯ ≪≫ asIso (pushoutSection ⋯ hVU ⋯ ⋯))
e : (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)] (↑Γ(X, f ⁻¹ᵁ U) : Type u) ≃ₐ[(↑Γ(Y, V) : Type u)]
  (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u) :=
  let __RingEquiv := e₀.commRingCatIsoToRingEquiv;
  { toEquiv := __RingEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
ψ : (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
    ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →ₐ[(↑Γ(Y, V) : Type u)]
  ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)) :=
  (↑e.mapIntegralClosure :
        ↥(integralClosure (↑Γ(Y, V) : Type u)
              ((↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)] (↑Γ(X, f ⁻¹ᵁ U) : Type u))) →ₐ[(↑Γ(Y, V) : Type u)]
          ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))).comp
    (toIntegralClosure (↑Γ(S, U) : Type u) (↑Γ(Y, V) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))
hψ :
  Function.Bijective (α :=
    (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)] ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) (β :=
    ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))
    (⇑ψ :
      (a :
          (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)] ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) →
        ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))
φ : pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU) ⟶
  Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W) :=
  CategoryStruct.comp (Y :=
    pushout (Y := CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))
      (CommRingCat.ofHom
        (algebraMap (↑Γ(S, U) : Type u) ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
      (appLE g U V hVU))
    (pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
      (CommRingCat.ofHom
        (algebraMap (↑Γ(S, U) : Type u) ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
      (appLE g U V hVU) (Iso.hom (normalizationObjIso f hU)) (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯)
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        ((↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)] ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
      (Iso.inv (IsPushout.isoPushout ⋯))
      ((RingEquiv.toCommRingCatIso (RingEquiv.ofBijective ψ.toRingHom hψ)).hom ≫
        CategoryStruct.comp (Y := Γ(normalization (pullback.snd f g), fromNormalization (pullback.snd f g) ⁻¹ᵁ V))
          (Iso.inv (normalizationObjIso (pullback.snd f g) hV))
          ((normalization (X := pullback f g) (pullback.snd f g)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))))
h :
  appLE (fromNormalization (pullback.snd f g)) V (normalizationPullback f g ⁻¹ᵁ W) ⋯ =
    CategoryStruct.comp (Y :=
      CommRingCat.of
        ((↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)] ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
      (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)
      (CategoryStruct.comp (Y :=
        CommRingCat.of ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))
        (CommRingCat.ofHom
          (↑(RingEquiv.ofBijective
                (↑ψ :
                  (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
                      ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+*
                    ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))
                hψ) :
            (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
                ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+*
              ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))))
        (CategoryStruct.comp (Y := Γ(normalization (pullback.snd f g), fromNormalization (pullback.snd f g) ⁻¹ᵁ V))
          (Iso.inv (normalizationObjIso (pullback.snd f g) hV))
          ((normalization (X := pullback f g) (pullback.snd f g)).presheaf.map (eqToHom ⋯))))
⊢ Eq (α := Γ(Y, V) ⟶ Γ(normalization (pullback.snd f g), normalizationPullback f g ⁻¹ᵁ W))
    (CategoryStruct.comp (Y :=
      pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU))
      (pushout.inr (app (fromNormalization f) U) (appLE g U V hVU))
      (pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
          (appLE (fromNormalization f) U (fromNormalization f ⁻¹ᵁ U) ⋯) (appLE g U V hVU)
          (𝟙 Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯ ≫
        pushoutSection ⋯ hVU ⋯ ⋯ ≫ app (normalizationPullback f g) W))
    (CategoryStruct.comp (Y :=
      pushout (Y := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U) (appLE g U V hVU))
      (pushout.inr (app (fromNormalization f) U) (appLE g U V hVU))
      (CategoryStruct.comp (Y :=
        pushout (Y := CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))
          (CommRingCat.ofHom
            (algebraMap (↑Γ(S, U) : Type u) ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
          (appLE g U V hVU))
        (pushout.map (app (fromNormalization f) U) (appLE g U V hVU)
          (CommRingCat.ofHom
            (algebraMap (↑Γ(S, U) : Type u) ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
          (appLE g U V hVU) (Iso.hom (normalizationObjIso f hU)) (𝟙 Γ(Y, V)) (𝟙 Γ(S, U)) ⋯ ⋯)
        (CategoryStruct.comp (Y :=
          CommRingCat.of
            ((↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
              ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
          (Iso.inv (IsPushout.isoPushout ⋯))
          (CategoryStruct.comp (Y :=
            CommRingCat.of ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))
            (CommRingCat.ofHom
              (↑(RingEquiv.ofBijective
                    (↑ψ :
                      (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
                          ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+*
                        ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))
                    hψ) :
                (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
                    ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+*
                  ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))))
            (CategoryStruct.comp (Y := Γ(normalization (pullback.snd f g), fromNormalization (pullback.snd f g) ⁻¹ᵁ V))
              (Iso.inv (normalizationObjIso (pullback.snd f g) hV))
              ((normalization (X := pullback f g) (pullback.snd f g)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))))))))

Tactic:
simp only [Scheme.Hom.app_eq_appLE, colimit.ι_desc_assoc, span_right, PushoutCocone.mk_pt,
      PushoutCocone.mk_ι_app, Category.id_comp, Scheme.Hom.appLE_comp_appLE,
      Scheme.Hom.normalizationPullback_snd, eqToHom_op, IsPushout.inr_isoPushout_inv_assoc]

Premises used: CategoryTheory.Limits.span_right, CategoryTheory.IsPushout.inr_isoPushout_inv_assoc, CategoryTheory.Limits.PushoutCocone.mk_ι_app, CategoryTheory.eqToHom_op, CategoryTheory.Limits.PushoutCocone.mk_pt, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.Limits.colimit.ι_desc_assoc, AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE, CategoryTheory.Category.id_comp