-- 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)))
⊢ 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) ⋯)).codRestrict
                              (integralClosure (↑Γ(Y, U.toOpens) : Type u) (↑Γ(X, f ⁻¹ᵁ U.toOpens) : Type u)) ⋯)) ≫
                        ⋯.fromSpec,
                    naturality := ⋯ :
                    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)
have simp : (f ⁻¹ᵁ (↑U : Y.Opens)).toSpecΓ ≫
    Spec.map
        (CategoryStruct.comp (Y :=
          CommRingCat.of ↥(integralClosure (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u)))
          (CommRingCat.ofHom
            ((CommRingCat.Hom.hom (appLE f₁ (f₂ ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ toOpens U) sorry)).codRestrict
              (integralClosure (↑Γ(Y, toOpens U) : Type u) (↑Γ(X, f ⁻¹ᵁ toOpens U) : Type u)) sorry))
          (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)))) ≫
      sorry.fromSpec =
  Opens.ι
      ((TopologicalSpace.Opens.comap (TopCat.Hom.hom f.base) :
          (a : TopologicalSpace.Opens ↥Y) → TopologicalSpace.Opens ↥X)
        (↑U : Y.Opens)) ≫
    f₁
Tactic: simp only [colimit.ι_desc, ← Spec.map_comp_assoc]