{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {ι' : Type u_2} →
        {X : ι → ι' → C} →
          (c : (i : ι) → CategoryTheory.Limits.Fan fun j => X i j) →
            ((i : ι) → CategoryTheory.Limits.IsLimit (c i)) →
              (c' : CategoryTheory.Limits.Fan fun i => (c i).pt) →
                CategoryTheory.Limits.IsLimit c' →
                  CategoryTheory.Limits.IsLimit
                    (CategoryTheory.Limits.Fan.mk c'.pt fun p =>
                      CategoryTheory.CategoryStruct.comp (c'.proj p.1) ((c p.1).proj p.2))