{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        {F : CategoryTheory.Functor J C} →
          {c₁ : CategoryTheory.Limits.Fan F.obj} →
            {c₂ : CategoryTheory.Limits.Fan fun f => F.obj f.fst.2} →
              (s t : c₁.pt ⟶ c₂.pt) →
                (hs :
                    ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                      CategoryTheory.CategoryStruct.comp s (c₂.π.app { as := f }) =
                        CategoryTheory.CategoryStruct.comp (c₁.π.app { as := f.fst.1 }) (F.map f.snd)) →
                  (ht :
                      ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
                        CategoryTheory.CategoryStruct.comp t (c₂.π.app { as := f }) = c₁.π.app { as := f.fst.2 }) →
                    {i : CategoryTheory.Limits.Fork s t} →
                      CategoryTheory.Limits.IsLimit c₁ →
                        CategoryTheory.Limits.IsLimit c₂ →
                          CategoryTheory.Limits.IsLimit i →
                            CategoryTheory.Limits.IsLimit
                              (CategoryTheory.Limits.HasLimitOfHasProductsOfHasEqualizers.buildLimit s t hs ht i)