-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U V : Y.AffineZariskiSite
i : U ⟶ V
this :
  Iso.inv (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
      Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑V : Y.Opens)) =
    X.homOfLE ⋯
rw :
  Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ normalization f)
    ((f ⁻¹ᵁ U.toOpens).toSpecΓ ≫
      CategoryStruct.comp (Y :=
        Spec
          (CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u))))
        (Spec.map
          (CommRingCat.ofHom
              (AlgHom.toRingHom
                (Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑V : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑V : Y.Opens)) : Type u)))) ≫
            X.presheaf.map (homOfLE ⋯).op))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) V))
    ((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))
⊢ Eq (α := (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X U ⟶ normalization f)
    (Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) i ≫
      (fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
          (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
              (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) :
            (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X U ⟶ normalization f))
        V)
    ((fun (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀) ↦
        (Iso.hom (pullbackRestrictIsoRestrict f (↑U : Y.Opens)) ≫
            (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) :
          (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X U ⟶ normalization f))
      U)

Tactic:
rw [← Iso.inv_comp_eq, reassoc_of% this, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc,
    ← Spec.map_comp_assoc]

Premises used: AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc, CategoryTheory.Iso.inv_comp_eq, AlgebraicGeometry.Spec.map_comp_assoc