∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  {X_1 Y_1 Z_1 : CategoryTheory.Limits.PushoutCocone f g} (f_1 : X_1 ⟶ Y_1) (g_1 : Y_1 ⟶ Z_1),
  { hom := CategoryTheory.Under.homMk (CategoryTheory.CategoryStruct.comp f_1 g_1).hom ⋯, w := ⋯ } =
    CategoryTheory.CategoryStruct.comp { hom := CategoryTheory.Under.homMk f_1.hom ⋯, w := ⋯ }
      { hom := CategoryTheory.Under.homMk g_1.hom ⋯, w := ⋯ }