∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X : CategoryTheory.SimplicialObject C}
  (s : SimplicialObject.Splitting X) [inst_1 : CategoryTheory.Preadditive C] (i j : ℕ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        ((s.cofan (Opposite.op (SimplexCategory.mk i))).inj
          (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk i))))
        (AlgebraicTopology.DoldKan.PInfty.f i))
      ((AlgebraicTopology.DoldKan.N₁.obj X).X.d i j) =
    CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex).X.d i j)
      (CategoryTheory.CategoryStruct.comp
        ((s.cofan (Opposite.op (SimplexCategory.mk j))).inj
          (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk j))))
        (AlgebraicTopology.DoldKan.PInfty.f j))