sum of inequalities of functions

Stream: new members

[Kyle Miller]

What's the best way to fill in this sorry?

import data.fintype.basic
import algebra.big_operators

open_locale big_operators

example {α : Type*} [fintype α] (f : α → ℕ) (g : α → ℕ) (h : ∀ a, f a ≤ g a) :
  ∑ a, f a ≤ ∑ a, g a :=
begin
  sorry,
end

[Johan Commelin]

I think there is finset.sum_le_sum

[Alex J. Best]

example {α : Type*} [fintype α] (f : α → ℕ) (g : α → ℕ) (h : ∀ a, f a ≤ g a) :
  ∑ a, f a ≤ ∑ a, g a :=  finset.sum_le_sum (λ x _ , h x)

[Bryan Gin-ge Chen]

How well does suggest do with this?

[Alex J. Best]

Not so well when I tried it, I didn't see anything useful from a quick look anyway.

[Kyle Miller]

I was editing things in algebra.big_operators.basic itself, so I wasn't able to see it with either library_search or suggest

[Kyle Miller]

Thanks for pointing me to it!

[Alex J. Best]

At least for me library search and suggest didn't work, I had to fall back to the old trusty of guess the name of a useful lemma!

[Kenny Lau]

kids these days with their suggest tactics