[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ f ≫ cokernel.π f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ kernel.ι f ≫ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0) = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ (kernel.ι f ≫ kernel.lift (cokernel.π f) f (_ : f ≫ cokernel.π f = 0)) ≫ equalizer.ι (cokernel.π f) 0 =
    0 ≫ equalizer.ι (cokernel.π f) 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ kernel.ι f ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ cokernel.desc (kernel.ι f) f (_ : kernel.ι f ≫ f = 0) ≫ cokernel.π f = 0
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coequalizer.π (kernel.ι f) 0 ≫ cokernel.desc (kernel.ι f) f (_ : kernel.ι f ≫ f = 0) ≫ cokernel.π f =
    coequalizer.π (kernel.ι f) 0 ≫ 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimageImageComparison f = coimageImageComparison' f
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u
inst✝³ : Category.{v, u} 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
[PROOFSTEP]
simp [coimageImageComparison, coimageImageComparison']
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasKernels C
inst✝ : HasCokernels C
P Q : C
f : P ⟶ Q
⊢ coimage.π f ≫ coimageImageComparison f ≫ image.ι f = f
[PROOFSTEP]
simp [coimageImageComparison]
