-- 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.Opens
hU : IsAffineOpen U
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u) := (CommRingCat.Hom.hom (app f U)).toAlgebra
this :
  IsIso (X := Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (Y :=
    Γ((normalizationOpenCover f).X ⟨U, hU⟩,
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ⁻¹ᵁ
        fromNormalization f ⁻¹ᵁ U))
    (app
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
      (fromNormalization f ⁻¹ᵁ U))
H :
  Eq (α :=
    (PreZeroHypercover.X (S := normalization f)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
        (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)).Opens)
    ⊤
    ((PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU) ≫
        fromNormalization f) ⁻¹ᵁ
      U)
⊢ Eq (α := Γ(Y, U) ⟶ Γ(normalization f, fromNormalization f ⁻¹ᵁ U)) (app (fromNormalization f) U)
    (CommRingCat.ofHom
        (algebraMap (↑(Y.presheaf.1 (Opposite.op U)) : Type u)
          ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) ≫
      Iso.inv (normalizationObjIso f hU))
have rw : (app
        (Spec.map
            ((normalizationDiagramMap f).app
              (Opposite.op (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens))) ≫
          IsAffineOpen.fromSpec sorry)
        U ≫
      (PreZeroHypercover.X (S := normalization f)
              (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
              (Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU)).presheaf.map
        (Quiver.Hom.op (eqToHom sorry))) ≫
    (PreZeroHypercover.X (S := normalization f)
            (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
            (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)).presheaf.map
      (Quiver.Hom.op (eqToHom H)) =
  ((CommRingCat.ofHom
          (algebraMap (↑(Y.presheaf.1 (Opposite.op U)) : Type u)
            ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))) ≫
        Iso.inv (normalizationObjIso f hU)) ≫
      app
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
          (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
        (fromNormalization f ⁻¹ᵁ U)) ≫
    (PreZeroHypercover.X (S := normalization f)
            (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
            (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU)).presheaf.map
      (Quiver.Hom.op (eqToHom H))
Tactic: rw [← cancel_mono (((normalizationOpenCover f).f ⟨U, hU⟩).app (f.fromNormalization ⁻¹ᵁ U)),
    ← Scheme.Hom.comp_app, Scheme.Hom.congr_app (f.ι_fromNormalization ⟨U, hU⟩) U,
    ← cancel_mono (((normalizationOpenCover f).X ⟨U, hU⟩).presheaf.map (eqToHom H).op)]