Reindexing sums

Stream: new members

[Julian Külshammer]

I want to prove the following lemma:

import algebra.group_with_zero.power
import algebra.big_operators.intervals

variable {α : Type}

open finset

open_locale big_operators

lemma somelemma [ring α] (x y : α) (n : ℕ): ∑ i in range n, x^i*y^(n-1-i)= ∑ j in range n, x^(n-1-j)*y^j :=
begin
  sorry
end

Using library_search I found rw ← sum_range_reflect as a possible first step. But then I wasn't able to convince lean that n-1-(n-1-j)=j because I wasn't able to apply nat.sub_sub_self since I didn't know how to extract the hypothesis that j\leq n-1 from the context. How can I do that or is there a better lemma to apply in mathlib?

[Patrick Massot]

Your second line should be refine sum_congr rfl (λ j j_in, _)

[Patrick Massot]

(after the rw you found)

[Patrick Massot]

You need to add import tactic at the top, and then

lemma somelemma [ring α] (x y : α) (n : ℕ): ∑ i in range n, x^i*y^(n-1-i)= ∑ j in range n, x^(n-1-j)*y^j :=
begin
  rw ← sum_range_reflect,
  refine sum_congr rfl (λ j j_in, _),
  rw mem_range at j_in,
  congr,
  omega
end

[Kevin Buzzard]

This sum_congr rfl trick comes up again and again, it's well worth knowing!

[Julian Külshammer]

Thanks a lot.

[Eric Wieser]

For more complex reindexings by different argument types, you want docs#finset.sum_bij