∀ {C : Type u_3} {ι : Type u_1} {J : Type u_5} [inst : CategoryTheory.Category.{u_2, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_5} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [inst_3 : ∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] (j : J) (i j_1 : ι),
  c.Rel i j_1 →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp (HomologicalComplex.eval C c i)) j)
        ((F.obj j).d i j_1) =
      CategoryTheory.CategoryStruct.comp
        ((((CategoryTheory.Functor.const J).obj
                  { X := fun n => CategoryTheory.Limits.limit (F.comp (HomologicalComplex.eval C c n)),
                    d := fun n m => CategoryTheory.Limits.limMap { app := fun j => (F.obj j).d n m, naturality := ⋯ },
                    shape := ⋯, d_comp_d' := ⋯ }).obj
              j).d
          i j_1)
        (CategoryTheory.Limits.limit.π (F.comp (HomologicalComplex.eval C c j_1)) j)