∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
  (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃) (X : C) {Z : C} (h : (CategoryTheory.shiftFunctor C a₁₂₃).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂).inv.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).inv.app X) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃).inv.app ((CategoryTheory.shiftFunctor C a₁).obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).inv.app X) h)