case h
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f = coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimageImageComparison f = coimageImageComparison' f
apply coequalizer.hom_ext
case h.h
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f) ≫ equalizer.ι (cokernel.π f) 0
case h
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f = coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f
apply equalizer.hom_ext
no goals
case h.h
C : Type u
inst✝³ : Category C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison f) ≫ equalizer.ι (cokernel.π f) 0 =
    (coequalizer.π (kernel.ι f) 0 ≫ coimageImageComparison' f) ≫ equalizer.ι (cokernel.π f) 0
simp [coimageImageComparison, coimageImageComparison']