no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X✝ Y X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d (obj X) (n + 1) n = ∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ X i
apply ChainComplex.of_d