∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C}
  (s : SimplicialObject.Splitting X) [inst_1 : CategoryTheory.Preadditive C] (n : ℕ),
  s.toKaroubiNondegComplexIsoN₁.inv.f.f n =
    s.πSummand (SimplicialObject.Splitting.IndexSet.id (Opposite.op (SimplexCategory.mk n)))