∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α =
    { obj := CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj,
      map := fun {X Y} β => { app := fun x => CategoryTheory.Limits.Sigma.map fun x_1 => β.app ↑x_1, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }