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