∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β),
  (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (s : Multiset α), s ≠ ∅ → f s.sum ≤ (Multiset.map f s).sum