∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Small.{u_1, u_2} R] (S : Submonoid R) {X Y Z : ModuleCat R} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  ModuleCat.localizedModuleMap S (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.localizedModuleMap S f) (ModuleCat.localizedModuleMap S g)