∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M N : ModuleCat R} (φ : M ⟶ N) {Z : ModuleCat R}
  (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars f).map φ)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf N).hom h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).hom
      (CategoryTheory.CategoryStruct.comp φ h)