The coproduct of a separating family of objects is separating

If a family of objects S : ι → C in a category with zero morphisms is separating, then the coproduct of S is a separator in C.

theorem CategoryTheory.IsSeparating.isSeparator_of_isColimit_cofan {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} {S : ι → C} (hS : IsSeparating (Set.range S)) {c : Limits.Cofan S} (hc : Limits.IsColimit c) : IsSeparator c.pt

theorem CategoryTheory.IsSeparating.isSeparator_coproduct {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] {ι : Type w} {S : ι → C} (hS : IsSeparating (Set.range S)) [Limits.HasCoproduct S] : IsSeparator (∐ S)