∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] {l : Filter α}
  {f : α → G}, Filter.Tendsto (fun x => -f x) l Filter.atTop = Filter.Tendsto f l Filter.atBot