∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y},
      CategoryTheory.IsUniversalColimit b →
        ∀ (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S)
          [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] [CategoryTheory.Limits.HasPullback u v]
          {P : ι × ι' → C} {q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i} {q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j},
          (∀ (i : ι) (j : ι'), CategoryTheory.IsPullback (q₁ i j) (q₂ i j) (f i) (g j)) →
            ∀ (d : CategoryTheory.Limits.Cofan P) (hd : CategoryTheory.Limits.IsColimit d),
              autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
                  CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit._auto_1 →
                autoParam (∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i)
                    CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit._auto_3 →
                  CategoryTheory.IsPullback
                    (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun p =>
                      CategoryTheory.CategoryStruct.comp (q₁ p.1 p.2) (a.inj p.1))
                    (CategoryTheory.Limits.Cofan.IsColimit.desc hd fun p =>
                      CategoryTheory.CategoryStruct.comp (q₂ p.1 p.2) (b.inj p.2))
                    u v