case a
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) (i + 2) 0
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ d C (i + 2) 0 = 0
rw [C.shape]
no goals
case a
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.down ℕ) (i + 2) 0
exact i.succ_succ_ne_one.symm