-- Module: Mathlib.AlgebraicGeometry.Normalization
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)
dsimp :
  ((app (IsAffineOpen.fromSpec ⋯) U ≫
          app (Spec.map ((normalizationDiagramMap f).app (Opposite.op U))) (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)) =
    (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 ⋯))) ≫
        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))
⊢ (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))

Tactic:
dsimp [normalizationObjIso]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationObjIso