ι : 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 : ι
f : (i j : ι) → X C i ⟶ X D j
j : ι
w : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ↑(prevD j) f = f j (ComplexShape.prev c j) ≫ d D (ComplexShape.prev c j) j
ι : 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 : ι
f : (i j : ι) → X C i ⟶ X D j
j j' : ι
w : ComplexShape.Rel c j' j
⊢ ↑(prevD j) f = f j j' ≫ d D j' j
obtain rfl := c.prev_eq' w
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 : ι
f : (i j : ι) → X C i ⟶ X D j
j : ι
w : ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ ↑(prevD j) f = f j (ComplexShape.prev c j) ≫ d D (ComplexShape.prev c j) j
rfl