∀ {α : Type u_2} {E : Type u_3} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [ContinuousAdd E] {f g : α → E}
  (m : E) {x : Filter α}, Filter.Tendsto f x (nhds m) → Filter.Tendsto (g - f) x (nhds 0) → Filter.Tendsto g x (nhds m)