-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
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 ⋯
⊢ 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)
have 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 sorry).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))
Tactic: rw [← Iso.inv_comp_eq, reassoc_of% this, ← Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc,
    ← Spec.map_comp_assoc]