case h
ι : Type u_1
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ (boundariesMap f i ≫ boundariesToCycles C₂ i) ≫ Subobject.arrow (cycles C₂ i) =
    (boundariesToCycles C₁ i ≫ cyclesMap f i) ≫ Subobject.arrow (cycles C₂ i)
ι : Type u_1
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ boundariesMap f i ≫ boundariesToCycles C₂ i = boundariesToCycles C₁ i ≫ cyclesMap f i
ext
no goals
case h
ι : Type u_1
V : Type u
inst✝⁴ : Category V
inst✝³ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝² : HasEqualizers V
inst✝¹ : HasImages V
inst✝ : HasImageMaps V
C₁ C₂ : HomologicalComplex V c
f : C₁ ⟶ C₂
i : ι
⊢ (boundariesMap f i ≫ boundariesToCycles C₂ i) ≫ Subobject.arrow (cycles C₂ i) =
    (boundariesToCycles C₁ i ≫ cyclesMap f i) ≫ Subobject.arrow (cycles C₂ i)
simp