Comparing finite sums along an injection

Separate the pointwise estimate, reindexing, and enlargement of the index set.

theorem NavierStokesAndEuler.sum_le_sum_of_injOn {ι : Type u_1} {κ : Type u_2} {A : Type u_3} [DecidableEq κ] [AddCommMonoid A] [Preorder A] [AddLeftMono A] {s : Finset ι} {t : Finset κ} {f : ι → A} {g : κ → A} (e : ι → κ) (he : Set.InjOn e ↑s) (himage : Finset.image e s ⊆ t) (hbound : ∀ i ∈ s, f i ≤ g (e i)) (hnonnegative : ∀ j ∈ t, j ∉ Finset.image e s → 0 ≤ g j) : ∑ i ∈ s, f i ≤ ∑ j ∈ t, g j