no goals
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map 0 ≫ F.map 0
rw [← Functor.map_comp, comp_zero]
no goals
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0
rw [Iso.hom_inv_id, Category.id_comp]
no goals
C : Type u₁
inst✝⁵ : Category C
D : Type u₂
inst✝⁴ : Category D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 = 0
simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]