no goals
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
⊢ 0 ≫ 𝟙 Y = 0
simp
case h
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
⊢ coequalizer.π 0 0 ≫ cokernelZeroIsoTarget.hom = coequalizer.π 0 0 ≫ cokernel.desc 0 (𝟙 Y) (_ : 0 ≫ 𝟙 Y = 0)
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
⊢ cokernelZeroIsoTarget.hom = cokernel.desc 0 (𝟙 Y) (_ : 0 ≫ 𝟙 Y = 0)
apply coequalizer.hom_ext
no goals
case h
C : Type u
inst✝² : Category C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
⊢ coequalizer.π 0 0 ≫ cokernelZeroIsoTarget.hom = coequalizer.π 0 0 ≫ cokernel.desc 0 (𝟙 Y) (_ : 0 ≫ 𝟙 Y = 0)
simp [cokernelZeroIsoTarget]