∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) {Z : C}
  (h : (CategoryTheory.shiftFunctor C n).obj (Opposite.unop X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor C n).map
        (CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f).unop)
      h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app Y).unop
      (CategoryTheory.CategoryStruct.comp f.unop h)