no goals
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ factorThruImage f = 0
simp [← cancel_mono (Limits.image.ι f)]
case h
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom =
    coequalizer.π (kernel.ι f) 0 ≫
      cokernel.desc (kernel.ι f) (factorThruImage f) (_ : kernel.ι f ≫ factorThruImage f = 0)
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (coimageIsoImage' f).hom = cokernel.desc (kernel.ι f) (factorThruImage f) (_ : kernel.ι f ≫ factorThruImage f = 0)
apply coequalizer.hom_ext
no goals
case h
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι f) 0 ≫ (coimageIsoImage' f).hom =
    coequalizer.π (kernel.ι f) 0 ≫
      cokernel.desc (kernel.ι f) (factorThruImage f) (_ : kernel.ι f ≫ factorThruImage f = 0)
simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc,
  Category.assoc, IsImage.lift_ι, coimageStrongEpiMonoFactorisation_m,
  Limits.image.fac]