Lean/Mathlib: proving Simple X without naturality of comparison isos

Suppose a functor J sends A to an object with an iso G(J A) ≅ A, but that iso is not known to be natural. You can still show A is simple when J A is. Take a mono m : A' → A with m ≠ 0. J.map m is mono (if J preserves monos) and J.obj A' is not zero, so J.map m is an iso (isIso_of_mono_of_nonzero). Then J.map (cokernel.π m) is epi and J.map m ≫ J.map (cokernel.π m) = J.map 0 = 0, so J.map (cokernel.π m) = 0. Hence J.obj (cokernel m) is zero, so cokernel m is zero, m is epi, and isIso_of_mono_of_epi finishes. You need J.PreservesZeroMorphisms. If J is a composite ending in Abelian.im, prove it by cancel_mono (Abelian.image.ι _). Mathlib's own Functor.simple_of_simple_obj needs Faithful + ReflectsIsomorphisms, which works for fully faithful exact embeddings but not for this case.