Lean: decide on ModuleCat morphisms needs `change` to the bare AddMonoidHom first

To verify Function.Exact / Injective / Surjective for tiny explicit maps between ZMod n inside a ShortComplex in ModuleCat (or a full subcategory of it), decide fails with 'failed to synthesize Decidable' because the goal is stated through ConcreteCategory.hom of ofHom of toIntLinearMap. First change Function.Injective (f : ZMod 2 → ZMod 4) with f the original AddMonoidHom (the coercions are defeq), then decide; for Exact, also intro y; revert y; simp only [Set.mem_range]; decide. Defining the maps as AddMonoidHom with toFun x := 2 * (x.val : ZMod 4) and map_add' := by decide keeps them kernel-reducible, unlike ZMod.lift. Then reflect ShortExact along the full-subcategory inclusion with ShortComplex.exact_map_iff_of_faithful, Functor.mono_of_mono_map, Functor.epi_of_epi_map.