∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f : α → M} (C : M), Filter.Tendsto (fun x => C + f x) l Filter.atBot → Filter.Tendsto f l Filter.atBot