-- 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)
⊢ (app
          (Spec.map
              ((normalizationDiagramMap f).app
                (Opposite.op (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens))) ≫
            IsAffineOpen.fromSpec ⋯)
          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 ⋯))) ≫
      (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))
have dsimp : ((app (IsAffineOpen.fromSpec sorry) U ≫
        app (Spec.map ((normalizationDiagramMap f).app (Opposite.op U))) (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)) =
  (CategoryStruct.comp (Y := CommRingCat.of ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u)))
        (CommRingCat.ofHom
          (algebraMap (↑(Y.presheaf.1 (Opposite.op U)) : Type u)
            ↥(integralClosure (↑Γ(Y, U) : Type u) (↑Γ(X, f ⁻¹ᵁ U) : Type u))))
        ((Iso.inv
              (ΓSpecIso
                ((normalizationDiagram f).obj
                  (Opposite.op (toOpens (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))))) ≫
            Iso.inv
              (appIso
                (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
                  (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) U hU))
                ⊤)) ≫
          (normalization f).presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫
      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: dsimp [normalizationObjIso]