-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (hypothesis)
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₁ : (precoverage IsOpenImmersion).IsStableUnderBaseChange
pf₂ : ∀ (i : (directedCover Y).I₀), HasPullback f ((directedCover Y).f i)
pf₃ : ∀ (U : (Precoverage.ZeroHypercover.pullback₁ f (directedCover Y)).I₀), HasPullback f (↑U : Y.Opens).ι
⊢ Eq (α := pullback f (↑U : Y.Opens).ι ⟶ normalization f)
    ((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))
        ⋯)
    (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))
have 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))
Tactic: generalize_proofs _ _ _ _ H