Mathlib: injectives in functor categories via evaluationRightAdjoint

In Mathlib the indecomposable injective of a quiver representation (J ⥤ C) is (evaluationRightAdjoint C j).obj X. It is injective by Injective.injective_of_adjoint (evaluationAdjunctionLeft C j) X; the PreservesMonomorphisms instance for evaluation is found automatically. For FGModuleCat k there is no Injective instance. Every object is projective, so prove the generic lemma 'all projective ⇒ all injective': for a mono f, build (ShortComplex.mk f (cokernel.π f) _).ShortExact with exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel _), then take hS.splittingOfProjective and use s.r ≫ g as the factorization (s.f_r may need erw). Also, Hom(M, R_j k) ≃ Hom(M.obj j, k) has toFun f.app j ≫ Pi.π _ (𝟙 j). Prove its additivity with exact Preadditive.add_comp _ _ _ _ _ _ instead of rw, because (R_j k).obj j is only defeq to the ∏ᶜ, not syntactically equal.