-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : QuasiSeparated f
T : Scheme
f₁ f₂ : normalization f ⟶ T
g : T ⟶ Y
inst_2 : IsAffineHom g
H₁ : toNormalization f ≫ f₁ = toNormalization f ≫ f₂
hf₁ : f₁ ≫ g = fromNormalization f
hf₂ : f₂ ≫ g = fromNormalization f
U :
  PreZeroHypercover.I₀ (S := normalization f)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
this_1 : Algebra (↑Γ(Y, (↑U : Y.Opens)) : Type u) (↑Γ(X, f ⁻¹ᵁ (↑U : Y.Opens)) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (app f (↑U : Y.Opens)))
this_2 : IsAffineHom f₁
this_3 : IsAffineHom f₂
f₀ : X ⟶ T := toNormalization f ≫ f₁
hf₀ : f₀ = toNormalization f ≫ f₂
h₁ : f ⁻¹ᵁ (↑U : Y.Opens) ≤ f₀ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₁' : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂ : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₁ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₂' : fromNormalization f ⁻¹ᵁ (↑U : Y.Opens) = f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)
h₃ : f ⁻¹ᵁ (↑U : Y.Opens) = toNormalization f ⁻¹ᵁ fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)
this :
  appLE (toNormalization f) (f₂ ⁻¹ᵁ g ⁻¹ᵁ (↑U : Y.Opens)) (f ⁻¹ᵁ (↑U : Y.Opens)) ⋯ =
    (normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
      app (toNormalization f) (fromNormalization f ⁻¹ᵁ (↑U : Y.Opens)) ≫ X.presheaf.map (Quiver.Hom.op (eqToHom h₃))
simp :
  Spec.map (𝟙 Γ(X, f ⁻¹ᵁ (↑U : Y.Opens))) ≫
      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))))
        (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f))
            (Subtype.mk (p := fun (U : Y.Opens) ↦ IsAffineOpen U) (↑U : Y.Opens) ⋯) ≫
          f₂) =
    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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂
⊢ Spec.map
        ((normalization f).presheaf.map (Quiver.Hom.op (eqToHom h₂')) ≫
          (Iso.hom (normalizationObjIso f ⋯) ≫
              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)) ≫
                X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫
            X.presheaf.map (Quiver.Hom.op (eqToHom h₃))) ≫
      ⋯.fromSpec ≫ f₂ =
    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))) ≫
      PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (normalizationOpenCover f)) U ≫ f₂

Tactic:
simp [appIso_hom', IsAffineOpen.SpecMap_appLE_fromSpec_assoc _ _ (isAffineOpen_top (Spec _)),
        IsAffineOpen.fromSpec_top, normalizationObjIso, normalizationDiagram]

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.Spec, AlgebraicGeometry.Scheme.Hom.appIso_hom', AlgebraicGeometry.Scheme.Hom.normalizationObjIso, AlgebraicGeometry.Scheme.Hom.normalizationDiagram, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec_assoc, AlgebraicGeometry.IsAffineOpen.fromSpec_top