-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
R : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
M : PresheafOfModules.{v, v₁, u₁, u} R
U V W : Cᵒᵖ
i : U ⟶ V
j : V ⟶ W
x : (↑(M.obj U) : Type v)
rw :
  Eq (α := (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))) (M.obj W)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj U) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj U) : Type u)) (RingHom.id (↑(R.obj U) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (Y :=
            Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))) (M.obj W))
            (M.map i ≫
              (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).map (M.map j) ≫
                NatTrans.app
                  (Iso.inv
                    (ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map i)) (RingCat.Hom.hom (R.map j))
                      (RingCat.Hom.hom (R.map (i ≫ j))) ⋯))
                  (M.obj W)) :
          (a : (↑(M.obj U) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))).obj (M.obj W)) : Type v))
        x :
      (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))) (M.obj W)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj V) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj V) : Type u)) (RingHom.id (↑(R.obj V) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map j) :
          (a : (↑(M.obj V) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map j))).obj (M.obj W)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj U) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj U) : Type u)) (RingHom.id (↑(R.obj U) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M.map i) :
              (a : (↑(M.obj U) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).obj (M.obj V)) : Type v))
            x :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).obj (M.obj V)) : Type v)) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map j))).obj (M.obj W)) : Type v))
⊢ Eq (α := (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))) (M.obj W)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj U) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj U) : Type u)) (RingHom.id (↑(R.obj U) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (Y :=
            Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))) (M.obj W)) (M.map (i ≫ j)) :
          (a : (↑(M.obj U) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))).obj (M.obj W)) : Type v))
        x :
      (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (i ≫ j)))) (M.obj W)) : Type v))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj V) : Type u)) ↦
            LinearMap.{u, u, v, v} (R := (↑(R.obj V) : Type u)) (RingHom.id (↑(R.obj V) : Type u)) (↑x1 : Type v)
              (↑x2 : Type v))
            (CC := ModuleCat.carrier) (M.map j) :
          (a : (↑(M.obj V) : Type v)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map j))).obj (M.obj W)) : Type v))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat.{v, u} (↑(R.obj U) : Type u)) ↦
                LinearMap.{u, u, v, v} (R := (↑(R.obj U) : Type u)) (RingHom.id (↑(R.obj U) : Type u)) (↑x1 : Type v)
                  (↑x2 : Type v))
                (CC := ModuleCat.carrier) (M.map i) :
              (a : (↑(M.obj U) : Type v)) →
                (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).obj (M.obj V)) : Type v))
            x :
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map i))).obj (M.obj V)) : Type v)) :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map j))).obj (M.obj W)) : Type v))

Tactic:
rw [M.map_comp]

Premises used: PresheafOfModules.map_comp