ι : 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
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ↑(dNext i) f = d C i (ComplexShape.next c i) ≫ f (ComplexShape.next c i) i
ι : 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
i i' : ι
w : ComplexShape.Rel c i i'
⊢ ↑(dNext i) f = d C i i' ≫ f i' i
obtain rfl := c.next_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
i : ι
w : ComplexShape.Rel c i (ComplexShape.next c i)
⊢ ↑(dNext i) f = d C i (ComplexShape.next c i) ≫ f (ComplexShape.next c i) i
rfl