-- 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_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)
e_a :
  ∀ (x : (↑(CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) : Type u)),
    Eq (α := (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                  (AlgHom.toRingHom (Subalgebra.val (integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))) ≫
                appLE (pullback.fst f g) (f ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ V) H) :
            (a : (↑(CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) : Type u)) →
              (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
          x :
        (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
      ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                (RingHom.comp
                  (AlgHom.toRingHom
                    (Subalgebra.val
                      (integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))))
                  (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
                    (↑(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)))
                    (↑Algebra.TensorProduct.includeRight :
                      ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+*
                        (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
                          ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))))) :
            (a : (↑(CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) : Type u)) →
              (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
          x :
        (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
⊢ Eq (α :=
    CommRingCat.of ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) ⟶
      Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V))
    (CommRingCat.ofHom
        (AlgHom.toRingHom (Subalgebra.val (integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))) ≫
      appLE (pullback.fst f g) (f ⁻¹ᵁ U) (pullback.snd f g ⁻¹ᵁ V) H)
    (CommRingCat.ofHom
      (RingHom.comp
        (AlgHom.toRingHom
          (Subalgebra.val (integralClosure (↑Γ(Y, V) : Type u) (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))))
        (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
          (↑(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)))
          (↑Algebra.TensorProduct.includeRight :
            ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)) →+*
              (↑Γ(Y, V) : Type u) ⊗[(↑Γ(S, U) : Type u)]
                ↥(integralClosure (↑Γ(S, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))))

Tactic:
ext x