∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (g : (i j : ι) → D.X i ⟶ E.X j) (j : ι),
  ((prevD j) fun i j => CategoryTheory.CategoryStruct.comp (f.f i) (g i j)) =
    CategoryTheory.CategoryStruct.comp (f.f j) ((prevD j) g)