no goals
ι : Type u_1
V : Type u
inst✝² : Category V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
C₁ C₂ C₃ : HomologicalComplex V c
f✝ f : C₁ ⟶ C₂
i : ι
⊢ cyclesMap f i ≫ Subobject.arrow (cycles C₂ i) = Subobject.arrow (cycles C₁ i) ≫ Hom.f f i
simp