-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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))
⊢ 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 ⋯))))
have h₁ : (normalization f).presheaf.map (Quiver.Hom.op (eqToHom sorry)) ≫
    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 sorry))) =
  (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 sorry))) ≫
    X.presheaf.map (Quiver.Hom.op (eqToHom H))
Tactic: convert! congr($(Scheme.Hom.congr_app (f.ι_toNormalization U) (f.fromNormalization ⁻¹ᵁ U)) ≫
    X.presheaf.map (eqToHom H).op) using 1