∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] [inst_2 : CategoryTheory.Limits.HasPushout f.op g.op],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.op g.op)
      (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op =
    (CategoryTheory.Limits.pullback.fst f g).op