∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : AddMonoid β] [inst_2 : Preorder β] [AddLeftMono β]
  (l : List α) (f : α → β), f 1 ≤ 0 → (∀ (a b : α), f (a * b) ≤ f a + f b) → f l.prod ≤ (List.map f l).sum