case h
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ (imageMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    (cokernel.π (kernel.ι f) ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ (imageMonoFactorisation f).e = cokernel.π (kernel.ι f) ≫ coimageImageComparison f
apply equalizer.hom_ext
no goals
case h
C : Type u
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ (imageMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    (cokernel.π (kernel.ι f) ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0
simp only [Abelian.coimageImageComparison, imageMonoFactorisation_e, Category.assoc,
  cokernel.π_desc_assoc]