∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (self : PresheafOfModules R) {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : ModuleCat ↑(R.obj X)}
  (h :
    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g)))).obj (self.obj Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (self.map f)
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (self.map g))
        (CategoryTheory.CategoryStruct.comp
          ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
            (self.obj Z))
          h))