-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
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 : Cᵒᵖ),
    Small.{v, max u₂ v}
      (↑((F ⋙ evaluation R X) ⋙
              forget (ModuleCat.{v, u} (↑(R.obj X) : Type u)) (FC :=
                fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj X) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj X) : Type u)) (RingHom.id (↑(R.obj X) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier)).sections :
        Type (max u₂ v))
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
j : J
w :
  Eq (α :=
    limit (F ⋙ evaluation R X) ⟶
      Functor.obj ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j)
    (CategoryStruct.comp (Y :=
      limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
      (limMap (F.whiskerLeft (restriction R (f ≫ g))))
      (limit.π ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j))
    (CategoryStruct.comp (Y := limit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
      (limMap (F.whiskerLeft (restriction R f)) :
        limit (F ⋙ evaluation R X) ⟶
          limit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
      (CategoryStruct.comp (Y :=
          (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (limit (F ⋙ evaluation R Y)))
          (Iso.inv (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)))
          (CategoryStruct.comp (Y :=
            (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
              (limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g)))))
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (limMap (F.whiskerLeft (restriction R g))) :
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (limit (F ⋙ evaluation R Y)) ⟶
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
                  (limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g)))))
            (CategoryStruct.comp (Y :=
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
                  ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (limit (F ⋙ evaluation R Z))))
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                  (Iso.inv
                    (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) (F ⋙ evaluation R Z))))
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                    ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).map (limit.π (F ⋙ evaluation R Z) j)) ≫
                  Iso.inv
                    (ModuleCat.restrictScalarsComp'App (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                      (RingCat.Hom.hom (R.map (f ≫ g))) ⋯ ((F ⋙ evaluation R Z).obj j))) :
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
                  (limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g)))) ⟶
                Functor.obj ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j)) :
        limit ((F ⋙ evaluation R Y) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
          Functor.obj ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j))
⊢ Eq (α :=
    limit (F ⋙ evaluation R X) ⟶
      Functor.obj (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j)
    (CategoryStruct.comp (Y := limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
      (limMap (F.whiskerLeft (restriction R (f ≫ g))))
      (limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j))
    (CategoryStruct.comp (Y := limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
      (CategoryStruct.comp (Y := limit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
          (limMap (F.whiskerLeft (restriction R f)) :
            limit (F ⋙ evaluation R X) ⟶
              limit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))))
          (CategoryStruct.comp (Y :=
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj (limit (F ⋙ evaluation R Y)))
              (Iso.inv (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) (F ⋙ evaluation R Y)))
              (CategoryStruct.comp (Y :=
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).obj
                  ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (limit (F ⋙ evaluation R Z))))
                ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map
                  (CategoryStruct.comp (Y :=
                    limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
                    (limMap (F.whiskerLeft (restriction R g)) :
                      limit (F ⋙ evaluation R Y) ⟶
                        limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))))
                    (Iso.inv
                        (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g)))
                          (F ⋙ evaluation R Z)) :
                      limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))) ⟶
                        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map g))).obj (limit (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))) ⋯ (limit (F ⋙ evaluation R Z))) ≫
                  Iso.hom
                    (preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))
                      (F ⋙ evaluation R Z)))) :
            limit (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))) ⟶
              limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g))))) :
        limit (F ⋙ evaluation R X) ⟶
          limit ((F ⋙ evaluation R Z) ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
      (limit.π (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j :
        Quiver.Hom (V := ModuleCat.{v, u} (↑(R.obj X) : Type u))
          (limit (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))))
          (Functor.obj (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (f ≫ g)))) j)))

Tactic:
simp only [Functor.map_comp, assoc, ← Functor.assoc, preservesLimitIso_hom_π,
      ← ModuleCat.restrictScalarsComp'App_inv_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.assoc, ModuleCat.restrictScalarsComp'App_inv_naturality, CategoryTheory.preservesLimitIso_hom_π, CategoryTheory.Functor.map_comp