∀ {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 : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)}
  (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      (({ obj := fun c => CategoryTheory.Limits.PushoutCocone.mk c.inl.right c.inr.right ⋯,
                map := fun {c₁ c₂} a => { hom := a.hom.right, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp
            {
              obj := fun c =>
                CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯)
                  (CategoryTheory.Under.homMk c.inr ⋯),
              map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
              map_comp := ⋯ }).map
        f_1)
      ((fun X_2 =>
            CategoryTheory.Limits.BinaryCofan.ext
              (CategoryTheory.Under.isoMk
                (CategoryTheory.Iso.refl
                  (({ obj := fun c => CategoryTheory.Limits.PushoutCocone.mk c.inl.right c.inr.right ⋯,
                                map := fun {c₁ c₂} a => { hom := a.hom.right, w := ⋯ }, map_id := ⋯,
                                map_comp := ⋯ }.comp
                            {
                              obj := fun c =>
                                CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯)
                                  (CategoryTheory.Under.homMk c.inr ⋯),
                              map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.homMk a.hom ⋯, w := ⋯ },
                              map_id := ⋯, map_comp := ⋯ }).obj
                        X_2).pt.right)
                ⋯)
              ⋯ ⋯)
          Y_1).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X_2 =>
            CategoryTheory.Limits.BinaryCofan.ext
              (CategoryTheory.Under.isoMk
                (CategoryTheory.Iso.refl
                  (({ obj := fun c => CategoryTheory.Limits.PushoutCocone.mk c.inl.right c.inr.right ⋯,
                                map := fun {c₁ c₂} a => { hom := a.hom.right, w := ⋯ }, map_id := ⋯,
                                map_comp := ⋯ }.comp
                            {
                              obj := fun c =>
                                CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯)
                                  (CategoryTheory.Under.homMk c.inr ⋯),
                              map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.homMk a.hom ⋯, w := ⋯ },
                              map_id := ⋯, map_comp := ⋯ }).obj
                        X_2).pt.right)
                ⋯)
              ⋯ ⋯)
          X_1).hom
      ((CategoryTheory.Functor.id
            (CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g))).map
        f_1)