{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {J₁ : Type u_3} →
        {J₂ : Type u_4} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} J₁] →
            [inst_3 : CategoryTheory.Category.{v_4, u_4} J₂] →
              {F₁ : CategoryTheory.Functor J₁ C} →
                {F₂ : CategoryTheory.Functor J₂ C} →
                  {c₁ : CategoryTheory.Limits.Cocone F₁} →
                    {c₂ : CategoryTheory.Limits.Cocone F₂} →
                      [CategoryTheory.Limits.PreservesColimit₂ F₁ F₂
                            (CategoryTheory.MonoidalCategory.curriedTensor C)] →
                        CategoryTheory.Limits.IsColimit c₁ →
                          CategoryTheory.Limits.IsColimit c₂ → CategoryTheory.Limits.IsColimit (c₁.tensor₂ c₂)