C : Type u_2
inst✝² : Category C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }).inv ≫ prod.snd = 𝟙 X
C : Type u_2
inst✝² : Category C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (zeroProdIso X).inv ≫ prod.snd = 𝟙 X
dsimp [zeroProdIso, binaryFanZeroLeft]
no goals
C : Type u_2
inst✝² : Category C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }).inv ≫ prod.snd = 𝟙 X
simp