-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules.{v, v₁, u₁, u} R
inst_2 :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst_3 : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
⊢ Eq (α :=
    (F.obj j).obj X ⟶
      Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
    (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R X)) (colimit.ι (F ⋙ evaluation R X) j)
      (CategoryStruct.comp (Y :=
        colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
        (colimMap (F.whiskerLeft (restriction R (f ≫ g))))
        (Iso.inv
          (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)))))
    (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R X)) (colimit.ι (F ⋙ evaluation R X) j)
      (CategoryStruct.comp (Y :=
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y)))
        (CategoryStruct.comp (Y := colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
          (colimMap (F.whiskerLeft (restriction R f)) :
            colimit (F ⋙ evaluation R X) ⟶
              colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
          (Iso.inv (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)) :
            colimit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y))))
        ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
            (CategoryStruct.comp (Y :=
              colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
              (colimMap (F.whiskerLeft (restriction R g)) :
                colimit (F ⋙ evaluation R Y) ⟶
                  colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
              (Iso.inv
                  (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)) :
                colimit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) ⟶
                  (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (colimit (F ⋙ evaluation R Z)))) ≫
          Iso.inv
            (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
              (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ (colimit (F ⋙ evaluation R Z))))))
have rw : Eq (α :=
  (F.obj j).obj X ⟶
    Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z)))
  (CategoryStruct.comp (Y :=
    Functor.obj (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j)
    ((F.obj j).map (f ≫ g))
    (CategoryStruct.comp (Y :=
      colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
      (colimit.ι (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j)
      (Iso.inv
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (F ⋙ evaluation R Z)))))
  ((F.whiskerLeft (restriction R f)).app j ≫
    CategoryStruct.comp (Y := colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
      (colimit.ι (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) j :
        (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj j ⟶
          colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
      (CategoryStruct.comp (Y :=
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (colimit (F ⋙ evaluation R Y)))
          (Iso.inv (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)))
          ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
              (CategoryStruct.comp (Y :=
                colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
                (colimMap (F.whiskerLeft (restriction R g)) :
                  colimit (F ⋙ evaluation R Y) ⟶
                    colimit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
                (Iso.inv
                    (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z)) :
                  colimit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) ⟶
                    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (colimit (F ⋙ evaluation R Z)))) ≫
            Iso.inv
              (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (f ≫ g))) sorry (colimit (F ⋙ evaluation R Z)))) :
        colimit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
          Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) (colimit (F ⋙ evaluation R Z))))
Tactic: rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app, assoc, ι_colimMap_assoc]