-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
U : (↑Y.affineOpens : Type u)
pf : HasPullback f (↑U : Y.Opens).ι
pf_1 : (precoverage IsOpenImmersion).IsStableUnderBaseChange
pf_2 : ∀ (i : (directedCover Y).I₀), HasPullback f ((directedCover Y).f i)
pf_3 : ∀ (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀), HasPullback f (↑U : Y.Opens).ι
H :
  ∀ {i j : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀} (hij : i ⟶ j),
    Eq (α := (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).X i ⟶ normalization f)
      (Cover.trans (P := IsOpenImmersion) (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)) hij ≫
        Iso.hom (pullbackRestrictIsoRestrict f (↑j : Y.Opens)) ≫
          (f ⁻¹ᵁ (↑j : Y.Opens)).toSpecΓ ≫
            CategoryStruct.comp (Y :=
              Spec
                (CommRingCat.of
                  ↥(integralClosure (↑Γ(Y, (↑j : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑j : Y.Opens)) : Type u))))
              (Spec.map
                (CommRingCat.ofHom
                  (AlgHom.toRingHom
                    (Subalgebra.val
                      (integralClosure (↑Γ(Y, (↑j : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑j : Y.Opens)) : Type u))))))
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) j))
      (Iso.hom (pullbackRestrictIsoRestrict f (↑i : Y.Opens)) ≫
        (f ⁻¹ᵁ (↑i : Y.Opens)).toSpecΓ ≫
          CategoryStruct.comp (Y :=
            Spec
              (CommRingCat.of
                ↥(integralClosure (↑Γ(Y, (↑i : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑i : Y.Opens)) : Type u))))
            (Spec.map
              (CommRingCat.ofHom
                (AlgHom.toRingHom
                  (Subalgebra.val
                    (integralClosure (↑Γ(Y, (↑i : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑i : Y.Opens)) : Type u))))))
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) i))
⊢ (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).f U ≫
      OpenCover.glueMorphismsOfLocallyDirected (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y))
        (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))
        @H =
    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)

Tactic:
Scheme.OpenCover.map_glueMorphismsOfLocallyDirected _ _ H _

Premises used: Set.Mem, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOfLocallyDirected, setOf, AlgebraicGeometry.Scheme.restrict, CategoryTheory.Limits.limit, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.toScheme