∀ {C₁ : Type u_6} {C₂ : Type u_2} {C₃ : Type u_4} [inst : CategoryTheory.Category.{u_5, u_6} C₁]
  [inst_1 : CategoryTheory.Category.{u_1, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_3, u_4} 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 x_1 : CategoryTheory.Arrow C₂) (x_2 : x ⟶ x_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CategoryTheory.Arrow C₂)).map x_2)
      {
        left :=
          adj₂.homEquiv
            (CategoryTheory.Limits.pushout.inl ((F.map X₁.hom).app ((CategoryTheory.Functor.id C₂).obj x_1.left))
              ((F.obj ((CategoryTheory.Functor.id C₁).obj X₁.left)).map x_1.hom)),
        right :=
          CategoryTheory.Limits.pullback.lift
            (adj₂.homEquiv
              (CategoryTheory.Limits.pushout.inr ((F.map X₁.hom).app ((CategoryTheory.Functor.id C₂).obj x_1.left))
                ((F.obj ((CategoryTheory.Functor.id C₁).obj X₁.left)).map x_1.hom)))
            (adj₂.homEquiv
              (CategoryTheory.CategoryStruct.id
                ((F.obj ((CategoryTheory.Functor.id C₁).obj (Opposite.unop (Opposite.op X₁)).right)).obj
                  ((CategoryTheory.Functor.id (CategoryTheory.Arrow C₂)).obj x_1).right)))
            ⋯,
        w := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      {
        left :=
          adj₂.homEquiv
            (CategoryTheory.Limits.pushout.inl ((F.map X₁.hom).app ((CategoryTheory.Functor.id C₂).obj x.left))
              ((F.obj ((CategoryTheory.Functor.id C₁).obj X₁.left)).map x.hom)),
        right :=
          CategoryTheory.Limits.pullback.lift
            (adj₂.homEquiv
              (CategoryTheory.Limits.pushout.inr ((F.map X₁.hom).app ((CategoryTheory.Functor.id C₂).obj x.left))
                ((F.obj ((CategoryTheory.Functor.id C₁).obj X₁.left)).map x.hom)))
            (adj₂.homEquiv
              (CategoryTheory.CategoryStruct.id
                ((F.obj ((CategoryTheory.Functor.id C₁).obj (Opposite.unop (Opposite.op X₁)).right)).obj
                  ((CategoryTheory.Functor.id (CategoryTheory.Arrow C₂)).obj x).right)))
            ⋯,
        w := ⋯ }
      (((F.leibnizPushout.obj X₁).comp (G.leibnizPullback.obj (Opposite.op X₁))).map x_2)