∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {P Q : C} (R : C)
  (f : P ⟶ Q) (g g' : Q ⟶ R),
  (fun g => CategoryTheory.CategoryStruct.comp f g) (g + g') =
    (fun g => CategoryTheory.CategoryStruct.comp f g) g + (fun g => CategoryTheory.CategoryStruct.comp f g) g'