Tactics for big operators

Stream: new members

[Walter Moreira]

I'm playing with the big operators, and I'm having trouble finding the right tactics to operate on its elements. In the following dummy example, I'm guessing the first step will use some combination of sum_range_succ' (even though I haven't figured it out yet). But my main question is the second sorry. How can I apply some tactic like ring inside of the big operator?

import data.finset
import algebra.big_operators
import tactic

open_locale big_operators

example (R : Type*) [nonzero_comm_ring R] (n : ℕ) (u v : R) (h : u * v = 1)
    : ∑ i in finset.range (n + 2), u * v^i = u + ∑ i in finset.range (n + 1), v^i :=
begin
calc
    ∑ i in finset.range (n + 2), u * v^i  = u + ∑ i in finset.range (n + 1), u * v^(i + 1) : by sorry
    ... = u + ∑ i in finset.range (n + 1), v^i : by sorry
end

[Yury G. Kudryashov]

second step should be by simp only [pow_succ, mul_assoc, h, one_mul], possibly with pow_succ' and/or ← before mul_assoc.

[Yury G. Kudryashov]

In the first step the only difficulty with applying sum_range_succ' is that you have n + 2 while you need n + 1 + 1. The latter simplifies to the former but I'm not sure that they are defeq.

[Johan Commelin]

@Walter Moreira Another approach would be to start with rw finset.sum_congr rfl

[Johan Commelin]

After that it should be intros, straight_forward

[Walter Moreira]

Ah, I see. finset.sum_congr is exactly what I was looking for before embarking in the calc tactic. Thanks a lot!

By the way, is straight_forward a tactic? Or you just mean that it's easy from then on?

[Thanks @Yury G. Kudryashov for the hint on simp as well]

[Johan Commelin]

I mean it's easy. (It should be a tactic)

[Johan Commelin]

(Just like we've been wishing for schoolkid and undergrad....)

[Johan Commelin]

But using Yury's approach, you could probably get rid of the entire calc block, and prove it in a 1-line simp call.