C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d
      (ChainComplex.of (fun n => X.obj [n].op) (AlternatingFaceMapComplex.objD X)
        (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0))
      (n + 1) n =
    AlternatingFaceMapComplex.objD X n
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d ((alternatingFaceMapComplex C).obj X) (n + 1) n = AlternatingFaceMapComplex.objD X n
dsimp only [alternatingFaceMapComplex, AlternatingFaceMapComplex.obj]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ HomologicalComplex.d
      (ChainComplex.of (fun n => X.obj [n].op) (AlternatingFaceMapComplex.objD X)
        (_ : ∀ (n : ℕ), AlternatingFaceMapComplex.objD X (n + 1) ≫ AlternatingFaceMapComplex.objD X n = 0))
      (n + 1) n =
    AlternatingFaceMapComplex.objD X n
apply ChainComplex.of_d