ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject ((xPrevIso C r).hom ≫ d C i j) = imageSubobject (d C i j)
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject (dTo C j) = imageSubobject (d C i j)
rw [C.dTo_eq r]
no goals
ι : Type u_1
V : Type u
inst✝³ : Category V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : ComplexShape.Rel c i j
⊢ imageSubobject ((xPrevIso C r).hom ≫ d C i j) = imageSubobject (d C i j)
apply imageSubobject_iso_comp