Extracting indices out of sums

Stream: new members

[Hanting Zhang]

I'm trying to prove a lemma which essentially has the following form:

import ring_theory.polynomial.basic

open_locale big_operators
open finset

variables (k n : ℕ)

example (k n : ℕ) (f g : ℕ → ℕ) (h : k ≤ n → f k = g k) : ∑ l in range k, f l = ∑ l in range k, g l :=
begin
  sorry
end

"Obviously" l ≤ k ≤ n, so the hypothesis h is usable, but Lean complains that it has no idea what l is because it's not in the context. How do I extract data about about l? Is there any straightforward way to do this?

[Yakov Pechersky]

The sum shown has 'l' just for notation for (finset.range k).sum (fun l, f l)

[Yakov Pechersky]

There's probably some lemma about "sum_range_congr"

[Yakov Pechersky]

You can definitely apply "finset.sum_congr"

[Hanting Zhang]

Yes, that works. Thanks!