-- Module: Mathlib.AlgebraicGeometry.Normalization
Goal:
X Y : Scheme
f : X ⟶ Y
X_1 Y_1 Z : Y.Opensᵒᵖ
i : X_1 ⟶ Y_1
j : Y_1 ⟶ Z
simp_rw :
  Eq.{u + 1} (α :=
    CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u)) ⟶
      CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)))
    (CommRingCat.ofHom
      ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.map (homOfLE ⋯).op)).restrict
        (integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u))
        (integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)) ⋯))
    (CommRingCat.ofHom
      (@RingHom.comp _ ↥(integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u))
        _ _ Semiring.toNonAssocSemiring _
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
            (integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u))
            (integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)) ⋯ :
          ↥(integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u)) →+*
            ↥(integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
          (integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u))
          (integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u)) ⋯)))
⊢ Eq.{u + 1} (α :=
    CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u)) ⟶
      CommRingCat.of ↥(integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)))
    (CommRingCat.ofHom
      ((CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))).restrict
        (integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u))
        (integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)) ⋯))
    (CommRingCat.ofHom
      (@RingHom.comp _ ↥(integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u))
        _ _ Semiring.toNonAssocSemiring _
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
            (integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u))
            (integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)) ⋯ :
          ↥(integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u)) →+*
            ↥(integralClosure (↑Γ(Y, Opposite.unop Z) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Z) : Type u)))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)).restrict
          (integralClosure (↑Γ(Y, Opposite.unop X_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop X_1) : Type u))
          (integralClosure (↑Γ(Y, Opposite.unop Y_1) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop Y_1) : Type u)) ⋯)))

Tactic:
simp_rw [X.presheaf.map_comp]

Premises used: AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace