Zulip Chat Archive

Stream: new members

Topic: Extracting indices out of sums


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 22:22):

There's probably some lemma about "sum_range_congr"

view this post on Zulip Yakov Pechersky (Jan 05 2021 at 22:26):

You can definitely apply "finset.sum_congr"

view this post on Zulip Hanting Zhang (Jan 05 2021 at 22:29):

Yes, that works. Thanks!


Last updated: May 14 2021 at 12:18 UTC