-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ : X ⟶ T
f₂ : T ⟶ Y
inst_2 : IsIntegralHom f₂
H : f = f₁ ≫ f₂
U :
  (X.openCoverOfIsOpenCover
      (fun (k : (↑Y.affineOpens : Type u)) ↦
        (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
            (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑k : Y.Opens))
      ⋯).I₀
this : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app 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))))))
        (CategoryStruct.comp (Y := normalization f)
          (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U)
          (normalizationDesc f f₁ f₂ H)) =
    (X.openCoverOfIsOpenCover
            (fun (k : (↑Y.affineOpens : Type u)) ↦
              (TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
                  (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
                (↑k : Y.Opens))
            ⋯).f
        U ≫
      f₁
have dsimp : Eq (α := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ T)
  ((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
            (↑(Subalgebra.val
                  (integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))) :
              ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)) →+*
                (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u))))
        (CategoryStruct.comp (Y := normalization f) (colimit.ι (normalizationGlueData f).functor U)
          (colimit.desc (normalizationGlueData f).functor
            { pt := T,
              ι :=
                {
                  app := fun (U : Y.AffineZariskiSite) ↦
                    Spec.map
                        (CommRingCat.ofHom
                          ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ U.toOpens) sorry)).codRestrict
                            (integralClosure (↑Γ(Y, U.toOpens) : Type u) (↑Γ(X, f ⁻¹ᵁ U.toOpens) : Type u)) sorry)) ≫
                      sorry.fromSpec,
                  naturality := sorry :
                  NatTrans (normalizationGlueData f).functor (Functor.obj (Functor.const Y.AffineZariskiSite) T) } })) :
    (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ⟶ T)
  (Opens.ι
        ((TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
            (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
          (↑U : Y.Opens)) ≫
      f₁ :
    (↑((TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
              (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
            (↑U : Y.Opens)) :
        Scheme) ⟶
      T)
Tactic: dsimp [normalizationOpenCover, normalizationDesc]