∀ {k : Type u_3} [inst : Field k] {A : Type u_2} [inst_1 : Ring A] [inst_2 : Algebra k A] (X Y Z : ModuleCat A) (r : k)
  (f : X ⟶ Y) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g