-- Module: Mathlib.AlgebraicGeometry.Normalization
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)))
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) ⋯)).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)
⊢ (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₁

Tactic:
dsimp [normalizationOpenCover, normalizationDesc]

Premises used: AlgebraicGeometry.Scheme.Hom.normalizationDesc, AlgebraicGeometry.Scheme.Hom.normalizationOpenCover