-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
X_1 Y_1 Z : Y.Opensᵒᵖ
i : X_1 ⟶ Y_1
j : Y_1 ⟶ Z
⊢ 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)) ⋯)))
have 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 sorry).op ≫ (homOfLE sorry).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)) sorry))
  (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 sorry).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)) sorry :
        ↥(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 sorry).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)) sorry)))
Tactic: rw [← homOfLE_comp (f.preimage_mono j.unop.le) (f.preimage_mono i.unop.le), op_comp]