no goals
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
r : ComplexShape.Rel c i j
⊢ dFrom C i ≫ (xNextIso C r).hom = d C i j
simp [C.dFrom_eq r]