∀ {C₁ : Type u_6} {C₂ : Type u_4} {C₃ : Type u_2} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C₂] [inst_2 : CategoryTheory.Category.{u_1, u_2} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃))
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) (adj₂ : F ⊣₂ G) (X₁ : CategoryTheory.Arrow C₁)
  [inst_3 : CategoryTheory.Limits.HasPullbacks C₂] [inst_4 : CategoryTheory.Limits.HasPushouts C₃]
  (X₃ : CategoryTheory.Arrow C₃),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id C₃).map
        (CategoryTheory.Limits.pushout.desc
          (adj₂.homEquiv.symm
            (CategoryTheory.CategoryStruct.id
              ((CategoryTheory.Functor.id C₂).obj ((G.leibnizPullback.obj (Opposite.op X₁)).obj X₃).left)))
          (adj₂.homEquiv.symm
            (CategoryTheory.Limits.pullback.fst
              ((G.obj (Opposite.op ((CategoryTheory.Functor.id C₁).obj (Opposite.unop (Opposite.op X₁)).left))).map
                X₃.hom)
              ((G.map (Opposite.unop (Opposite.op X₁)).hom.op).app ((CategoryTheory.Functor.id C₃).obj X₃.right))))
          ⋯))
      ((CategoryTheory.Functor.id (CategoryTheory.Arrow C₃)).obj X₃).hom =
    CategoryTheory.CategoryStruct.comp
      (((G.leibnizPullback.obj (Opposite.op X₁)).comp (F.leibnizPushout.obj X₁)).obj X₃).hom
      ((CategoryTheory.Functor.id C₃).map
        (adj₂.homEquiv.symm
          (CategoryTheory.Limits.pullback.snd
            ((G.obj (Opposite.op ((CategoryTheory.Functor.id C₁).obj (Opposite.unop (Opposite.op X₁)).left))).map
              X₃.hom)
            ((G.map (Opposite.unop (Opposite.op X₁)).hom.op).app ((CategoryTheory.Functor.id C₃).obj X₃.right)))))