-- 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 ⋯ ⋯))
r : (↑Γ(Y, V) : Type u)
e_a : CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e₀.hom = app (pullback.snd f g) V
⊢ 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) (X := CommRingCat.of (↑(Y.presheaf.1 (Opposite.op V)) : Type u))
            (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom ≫ e₀.hom) :
          (a : (↑(CommRingCat.of (↑(Y.presheaf.1 (Opposite.op V)) : Type u)) : Type u)) →
            (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
        r :
      (↑Γ(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) (Y := Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V)) (app (pullback.snd f g) V) :
          (a : (↑Γ(Y, V) : Type u)) → (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))
        r :
      (↑Γ(pullback f g, pullback.snd f g ⁻¹ᵁ V) : Type u))

Tactic:
congr 2