-- 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)
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 ⋯)
          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))
⊢ 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))

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)]

Premises used: AlgebraicGeometry.Scheme.Hom.fromNormalization, CategoryTheory.PreZeroHypercover.f, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.Hom.congr_app, CategoryTheory.PreZeroHypercover.X, CategoryTheory.cancel_mono, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.Hom.ι_fromNormalization, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover, AlgebraicGeometry.Scheme.toLocallyRingedSpace