no goals
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f
simp [coimageImageComparison]