First isomorphism theorem for abelian categories

Stream: Is there code for X?

[Kevin Buzzard]

I appear to need the following variant. Do we have it? It's the last piece of the puzzle for one of the LTE files. Hopefully I didn't mess up...

import category_theory.abelian.basic
import category_theory.abelian.images

open category_theory category_theory.limits

variables {𝒞 : Type*} [category 𝒞] [abelian 𝒞]

-- possibly missing API
@[simp, reassoc] lemma kernel_ι_comp_factor_thru_image {A B : 𝒞} {f : A ⟶ B} :
kernel.ι f ≫ factor_thru_image f = 0 :=
comp_factor_thru_image_eq_zero (kernel.condition f)

lemma first_isomorphism_theorem {A B : 𝒞} (f : A ⟶ B) :
is_iso (cokernel.desc (kernel.ι f) (factor_thru_image f) (by simp)) :=
begin
  sorry,
end

[Markus Himmel]

I don't think we have this exact variant, but it's easy to prove:

begin
  convert (infer_instance : is_iso (abelian.coimage_iso_image' f).hom),
  simp [← cancel_mono (image.ι f), ← cancel_epi (cokernel.π (kernel.ι f))]
end