∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atTop → (∀ (x : α), 1 ≤ g x) → Filter.Tendsto (fun x => f x * g x) l Filter.atTop