∀ {J : Type u_2} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J SemiRingCat)
  [inst_1 : CategoryTheory.IsFiltered J] (t : CategoryTheory.Limits.Cocone F) (j : J),
  CategoryTheory.CategoryStruct.comp ((SemiRingCat.FilteredColimits.colimitCocone F).ι.app j)
      (SemiRingCat.ofHom
        (let __src := SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom t;
        { toFun := (↑__src).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) =
    t.ι.app j