-- 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)))
H :
  toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) =
    (f ⁻¹ᵁ (↑U : Y.Opens)).ι ''ᵁ
      ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
h :
  app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) =
    app ((f ⁻¹ᵁ (↑U : Y.Opens)).ι ≫ toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom H))
h₁ :
  (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
          ((f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
            CategoryStruct.comp (Y :=
              Spec
                (CommRingCat.of
                  ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
              (Spec.map
                (CommRingCat.ofHom
                  (AlgHom.toRingHom
                    (Subalgebra.val
                      (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))))
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U))
          (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫
        (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom H))
⊢ 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 ⋯))))

Tactic:
convert! congr($(Scheme.Hom.congr_app (f.ι_toNormalization U) (f.fromNormalization ⁻¹ᵁ U)) ≫
    X.presheaf.map (eqToHom H).op) using 1

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.ι_toNormalization, AlgebraicGeometry.Scheme.Hom.congr_app, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace