∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : b + a = 0) [inst_5 : F.CommShift A] (X : D),
  (CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a).hom.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorCompIsoId C b a h).inv.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C a).map
          (adj.unit.app ((CategoryTheory.shiftFunctor C b).obj (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor C a).map
            (G.map
              ((CategoryTheory.Functor.commShiftIso F b).hom.app (G.obj ((CategoryTheory.shiftFunctor D a).obj X)))))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor C a).map
              (G.map
                ((CategoryTheory.shiftFunctor D b).map (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj X)))))
            ((CategoryTheory.shiftFunctor C a).map
              (G.map ((CategoryTheory.shiftFunctorCompIsoId D a b ⋯).hom.app X))))))