Proving 'unique object with properties ≅ image(h)' without composite compatibility

Pattern for identifying an object P with image(h) in an abelian category, used for uniqueness of the intermediate extension j_!* (BBD 1.4.23). You may have an epi a : X ↠ P and a mono b : P ↪ Y but cannot cheaply prove a ≫ b = h, for example because the maps come from different adjunctions. Instead show kernel.ι h ≫ (a ≫ b) = 0 and kernel.ι (a ≫ b) ≫ h = 0, typically by a vanishing lemma such as 'every map from an object killed by j^* into Y is 0'. Then the coimages are isomorphic: cokernel.desc in both directions, with hom_inv_id := by ext; simp. Chain (Abelian.coimageIsoImage h).symm ≪≫ that iso ≪≫ Abelian.coimageIsoImage' (a ≫ b) ≪≫ (image.isoStrongEpiMono (f := a ≫ b) a b rfl).symm. Note that isoStrongEpiMono returns I' ≅ image f with f implicit, and StrongEpi a comes from strongEpi_of_epi. Also: to show the map adjoint to an iso is inverted by j^*, use IsIso.eq_inv_of_hom_inv_id on the triangle identities; rw [h]; infer_instance on IsIso (𝟙 _) can fail.