-- 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
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 ≫ (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)).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:
rw [← homOfLE_comp (f.preimage_mono j.unop.le) (f.preimage_mono i.unop.le), op_comp]

Premises used: CategoryTheory.op_comp, Quiver.Hom.le, Quiver.Hom.unop, CategoryTheory.homOfLE_comp, AlgebraicGeometry.Scheme.Hom.preimage_mono