finset.sum and injective maps

Stream: general

[Johan Commelin]

Random bit from LTE:

/-- The obvious embedding from `fin M` to `fin N` for `M ≤ N`. -/
private def ι {M N : ℕ} (h : M ≤ N) : fin M ↪ fin N := (fin.cast_le h).to_embedding

-- Should this be in mathlib?
lemma sum_eq_sum_map_ι {M N : ℕ} (h : M ≤ N) (f : fin N → ℝ≥0) :
  ∑ i, f (ι h i) = ∑ j in finset.map (ι h) finset.univ, f j :=
finset.sum_bij' (λ a _, ι h a) (λ a ha, by {rw mem_map, exact ⟨a, ha, rfl⟩})
(λ a ha, rfl) (λ a ha, ⟨a.1, begin
  rcases finset.mem_map.mp ha with ⟨⟨w,ww⟩,hw,rfl⟩,
  change w < M,
  linarith,
end ⟩)
(λ a ha, finset.mem_univ _) (λ a ha, by tidy) (λ a ha, by tidy)

[Johan Commelin]

Do we have a version of finset.sum_bij' for injective maps. Since \iota is injective, I feel like the proof of the lemma should be a 1-liner

[Johan Commelin]

Nevermind: finset.sum_map