## Stream: new members

### Topic: Extracting indices out of sums

#### Hanting Zhang (Jan 05 2021 at 22:12):

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 (Jan 05 2021 at 22:21):

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

#### Yakov Pechersky (Jan 05 2021 at 22:22):

There's probably some lemma about "sum_range_congr"

#### Yakov Pechersky (Jan 05 2021 at 22:26):

You can definitely apply "finset.sum_congr"

#### Hanting Zhang (Jan 05 2021 at 22:29):

Yes, that works. Thanks!

Last updated: May 14 2021 at 12:18 UTC