-- 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_1 : ↥(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_1 : ↥S)
V : TopologicalSpace.Opens ↥Y
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) ((pullback.snd (fromNormalization f) g) x_1 : ↥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_3 : 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 ⋯)))))
this :
  Mono.{u, u + 1} (X :=
    CommRingCat.of ↥(integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))) (Y :=
    CommRingCat.of (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
    (CommRingCat.ofHom
      (AlgHom.toRingHom
        (Subalgebra.val (integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u)))))
H : LE.le (α := (pullback f g).Opens) (pullback.snd f g ⁻¹ᵁ V) (pullback.fst f g ⁻¹ᵁ f ⁻¹ᵁ U)
x : (↑(CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) : Type u)
e_a :
  appLE (pullback.fst f g) (f ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ V) H =
    CommRingCat.ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ e₀.hom
⊢ Eq (α := (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (appLE (pullback.fst f g) (f ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ V) H) :
          (a : (↑Γ(X, f ⁻¹ᵁ U) : Type u)) → (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
        (↑x : (↑Γ(X, f ⁻¹ᵁ U) : Type u)) :
      (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := CommRingCat.of (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u))
            (CommRingCat.ofHom (AlgHom.toRingHom Algebra.TensorProduct.includeRight) ≫ e₀.hom) :
          (a : (↑(CommRingCat.of (↑(X.presheaf.1 (Opposite.op (f ⁻¹ᵁ U))) : Type u)) : Type u)) →
            (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
        (↑x : (↑Γ(X, f ⁻¹ᵁ U) : Type u)) :
      (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))

Tactic:
congr 2