∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {c₁ c₂ : CategoryTheory.Limits.PushoutCocone f g} (a : c₁ ⟶ c₂)
  (j : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c₁.inl ⋯)
              (CategoryTheory.Under.homMk c₁.inr ⋯)).ι.app
        j)
      (CategoryTheory.Under.homMk a.hom ⋯) =
    (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c₂.inl ⋯)
            (CategoryTheory.Under.homMk c₂.inr ⋯)).ι.app
      j