Stream: new members
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
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