Lean/Mathlib: transporting images along exact functors (intermediate extension)

To show F(image f) ≅ (something) for an exact functor F between abelian categories, use Abelian.PreservesImage.iso F f : F.obj (Abelian.image f) ≅ Abelian.image (F.map f) from Limits/Preserves/Shapes/AbelianImages.lean. It lives in namespace CategoryTheory.Abelian, so a bare PreservesImage.iso gives Unknown identifier. Its Preserves(Co)Limit hypotheses are found automatically from PreservesFiniteLimits/Colimits instances. If F.map f is an iso, asIso (Abelian.image.ι (F.map f)) identifies the image with the target. Get Epi from epi_of_epi_fac (Abelian.image.fac _), then isIso_of_mono_of_epi. To prove F.map (G.map φ) is iso via a natural iso e : K ⋙ G' ≅ G ⋙ F, use (NatIso.isIso_map_iff e φ).1 (by dsimp; infer_instance). Adjunction gotcha: rw [adj.counit_naturality] often fails because the goal has (𝟭 U).obj W. Use have h := adj.counit_naturality f; dsimp at h; rw [h].