no goals
ι : Type u_1
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
j : ι
h : ¬ComplexShape.Rel c (ComplexShape.prev c j) j
⊢ (xPrevIsoSelf C h).inv ≫ dTo C j = 0
simp [h]