∀ {ι : Type u_3} {V : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D},
  f = g → ∀ (i : ι), f.f i = (dNext i) 0 + (prevD i) 0 + g.f i