C : Type u_2
inst✝² : Category C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫
      (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X }).hom =
    𝟙 X
C : Type u_2
inst✝² : Category C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X
dsimp [zeroCoprodIso, binaryCofanZeroLeft]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫
      (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X }).hom =
    𝟙 X
simp