Separating set in the category of ind-objects

We construct a separating set in the category of ind-objects and conclude that if C is small and additive, then Ind C has a separator.

theorem CategoryTheory.Ind.isSeparating_range_yoneda {C : Type u} [Category.{v, u} C] : (ObjectProperty.ofObj Ind.yoneda.obj).IsSeparating

theorem CategoryTheory.Ind.isSeparator_range_yoneda {C : Type u} [SmallCategory C] [Preadditive C] [Limits.HasFiniteColimits C] : IsSeparator (∐ Ind.yoneda.obj)