∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (c : CategoryTheory.Limits.PushoutCocone f g) (X_1 : C) (j : CategoryTheory.Limits.WalkingCospan),
  ((CategoryTheory.Limits.Cones.postcompose
                (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.cospanOp f g).symm
                    (CategoryTheory.yoneda.obj X_1)).hom).obj
            (CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.walkingSpanOpEquiv.symm.functor
              ((CategoryTheory.yoneda.obj X_1).mapCone (CategoryTheory.Limits.Cocone.op c)))).π.app
      j =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Iso.refl
          ((CategoryTheory.Limits.Cones.postcompose
                  (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.cospanOp f g).symm
                      (CategoryTheory.yoneda.obj X_1)).hom).obj
              (CategoryTheory.Limits.Cone.whisker CategoryTheory.Limits.walkingSpanOpEquiv.symm.functor
                ((CategoryTheory.yoneda.obj X_1).mapCone (CategoryTheory.Limits.Cocone.op c)))).pt).hom
      (((CategoryTheory.yoneda.obj X_1).mapCone c.op).π.app j)