-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
this : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
change :
  Eq (α :=
    (normalization f).presheaf.obj (Opposite.op (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens))) ⟶
      Γ(X, toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    (app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)))
    ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
      Iso.hom
          (appIso (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
            ⊤) ≫
        Iso.hom (ΓSpecIso (Opposite.unop (((toOpensFunctor Y).op ⋙ normalizationDiagram f).rightOp.obj U))) ≫
          CategoryStruct.comp (Y := CommRingCat.of (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))
            (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))))
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))))
⊢ app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) =
    CategoryStruct.comp (Y :=
      CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
      ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
        Iso.hom
            (appIso
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
                (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯))
              ⊤) ≫
          Iso.hom
            (ΓSpecIso
              ((normalizationDiagram f).obj
                (Opposite.op (toOpens (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯))))))
      (CommRingCat.ofHom
          (↑(Subalgebra.val (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
            ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
              (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))

Tactic:
change _ = f.normalization.presheaf.map (eqToHom (by simp [fromNormalization_preimage])).op ≫
      ((f.normalizationOpenCover.f U).appIso _).hom ≫
      (Scheme.ΓSpecIso _).hom ≫
      CommRingCat.ofHom (integralClosure ↑Γ(Y, ↑U) ↑Γ(X, f ⁻¹ᵁ ↑U)).val.toRingHom ≫
      X.presheaf.map (eqToHom (by simp [← Scheme.Hom.comp_preimage])).op

Premises used: CategoryTheory.PreZeroHypercover.f, CommRingCat.carrier, Quiver.Hom.op, CategoryTheory.eqToHom, Subalgebra.val, CommRingCat.ofHom, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgHom.toRingHom, integralClosure, Opposite.op, AlgebraicGeometry.Scheme.Hom.appIso, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Iso.hom, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover, AlgebraicGeometry.Scheme.Hom.normalization, AlgebraicGeometry.Scheme.toLocallyRingedSpace