no goals
ι : Type u_1
V : Type u
inst✝⁶ : Category V
inst✝⁵ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
inst✝⁴ : HasZeroObject V
W : Type u_3
inst✝³ : Category W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
F : V ⥤ W
inst✝ : Functor.Additive F
i j : ι
h : i ≠ j
X : V
⊢ Hom.f ((singleMapHomologicalComplex F c j).hom.app X) i = 0
simp [singleMapHomologicalComplex, h]