no goals
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬ComplexShape.Rel c i (ComplexShape.next c i)
⊢ dFrom C i ≫ (xNextIsoSelf C h).hom = 0
simp [h]