∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {A : Type u_3} {B : Type u_4} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] (φ : A →+ B) [inst_3 : CategoryTheory.HasShift C B] {D : Type u_6}
  [inst_4 : CategoryTheory.Category.{u_5, u_6} D] [inst_5 : CategoryTheory.HasShift D B]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G)
  (x : CategoryTheory.PullbackShift D φ),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.PullbackShift.natIsoId C φ).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.PullbackShift.natTrans φ adj.unit)
              (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ F G).hom)).app
        ((CategoryTheory.PullbackShift.functor φ G).obj x))
      ((CategoryTheory.PullbackShift.functor φ G).map
        ((CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ G F).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.PullbackShift.natTrans φ adj.counit)
                (CategoryTheory.NatTrans.PullbackShift.natIsoId D φ).inv)).app
          x)) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.PullbackShift.functor φ G).obj x)