∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] (F : CategoryTheory.Functor C A) {G : Type u_4} [inst_2 : AddGroup G]
  [inst_3 : CategoryTheory.HasShift C G] [inst_4 : F.ShiftSequence G] {X Y : C} {m : G}
  (f : X ⟶ (CategoryTheory.shiftFunctor C m).obj Y) (n : G) (hnm : n + m = 0) (a a' : G) (ha' : m + a = a'),
  CategoryTheory.CategoryStruct.comp ((F.shiftIso n a' a ⋯).hom.app X) (F.shiftMap f a a' ha') =
    (F.shift a').map
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map f)
        ((CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app Y))