Mathlib: functorial images in abelian categories via Abelian.im

To turn an objectwise construction X ↦ Abelian.image (φ X) into a functor, do not build image maps by hand. Mathlib has CategoryTheory.Abelian.im : Arrow C ⥤ C (Abelian/Basic.lean), whose obj f := Abelian.image f.hom. Define a functor A ⥤ Arrow C with obj X := Arrow.mk (φ X) and map f := Arrow.homMk (g₁ f) (g₂ f) (naturality square); map_id/map_comp close with ext <;> simp. Then compose with Abelian.im. The objects of the composite are definitionally your Abelian.image (φ X), so a rfl lemma connects the functor to the existing objectwise definition and all lemmas about it stay usable. There is also Abelian.coim and coimIsoIm if you need coimages.