C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ f = default
rw [← id_comp f, ← id_comp (0: X ⟶ Y), h, zero_comp, zero_comp]
no goals
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
simp only
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ f = default
rw [← comp_id f, ← comp_id (0 : Y ⟶  X), h, comp_zero, comp_zero]
no goals
C : Type u
inst✝² : Category C
D : Type u'
inst✝¹ : Category D
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : Y ⟶ X
⊢ 0 = default
simp only