{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (h : X ⟶ W) →
            [inst_1 : CategoryTheory.Epi h] →
              (x : W ⟶ Y) →
                (y : W ⟶ Z) →
                  (hhx : CategoryTheory.CategoryStruct.comp h x = f) →
                    (hhy : CategoryTheory.CategoryStruct.comp h y = g) →
                      (s : CategoryTheory.Limits.PushoutCocone f g) →
                        CategoryTheory.Limits.IsColimit s →
                          have reassoc₁ := ⋯;
                          have reassoc₂ := ⋯;
                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk s.inl s.inr ⋯)