∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K K' : ChainComplex C ℕ} (f : K ⟶ K') {Δ Δ' : SimplexCategory} (i : Δ ⟶ Δ') [inst_2 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i) (f.f Δ.len) =
    CategoryTheory.CategoryStruct.comp (f.f Δ'.len) (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K' i)