no goals
V : Type u
inst✝¹ : Category V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : HomologicalComplex.X C 0 ⟶ X
w : d C 1 0 ≫ f = 0
i j : ℕ
⊢ d (augment C f w) (i + 1) (j + 1) = d C i j
cases i <;> rfl