∀ (V : Type u_3) [inst : CategoryTheory.Category.{u_2, u_3} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {X Y : V} (f : X ⟶ Y) (i j_1 : ι),
  c.Rel i j_1 →
    CategoryTheory.CategoryStruct.comp
        (if h : i = j then
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
        else 0)
        ({ X := fun i => if i = j then Y else 0, d := fun x x_1 => 0, shape := ⋯, d_comp_d' := ⋯ }.d i j_1) =
      CategoryTheory.CategoryStruct.comp
        ({ X := fun i => if i = j then X else 0, d := fun x x_1 => 0, shape := ⋯, d_comp_d' := ⋯ }.d i j_1)
        (if h : j_1 = j then
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
        else 0)