Additional results about the liftToFinset construction

If f is a family of objects of C, then there is a canonical cocone whose cocone point is the coproduct of f and whose legs are given by the inclusions of the finite subcoproducts. If C is preadditive, then we can describe the legs of this cocone as finite sums of projections followed by inclusions.

theorem CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app_eq_sum {C : Type u} [Category.{v, u} C] [Preadditive C] [HasFiniteCoproducts C] {α : Type w} [DecidableEq α] (f : α → C) [HasCoproduct f] (S : Finset (Discrete α)) : (finiteSubcoproductsCocone f).ι.app S = ∑ a ∈ S.attach, CategoryStruct.comp (Sigma.π (fun (a : ↥S) => f (↑a).as) a) (Sigma.ι f (↑a).as)

theorem CategoryTheory.Limits.ProductsFromFiniteCofiltered.finiteSubproductsCocone_π_app_eq_sum {C : Type u} [Category.{v, u} C] [Preadditive C] [HasFiniteProducts C] {α : Type w} [DecidableEq α] (f : α → C) [HasProduct f] (S : (Finset (Discrete α))ᵒᵖ) : (finiteSubproductsCone f).π.app S = ∑ a ∈ (Opposite.unop S).attach, CategoryStruct.comp (Pi.π f (↑a).as) (Pi.ι (fun (a : ↥(Opposite.unop S)) => f (↑a).as) a)