case a
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 (i + 2)
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ d C 0 (i + 2) = 0
rw [C.shape]
case a
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬1 = i + 2
case a
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬ComplexShape.Rel (ComplexShape.up ℕ) 0 (i + 2)
simp only [ComplexShape.up_Rel, zero_add]
no goals
case a
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬1 = i + 2
exact (Nat.one_lt_succ_succ _).ne