# Zulip Chat Archive

## Stream: new members

### Topic: Tactics for big operators

#### Walter Moreira (Jun 01 2020 at 02:44):

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 (Jun 01 2020 at 02:53):

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 (Jun 01 2020 at 02:54):

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 (Jun 01 2020 at 02:57):

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

#### Johan Commelin (Jun 01 2020 at 02:58):

After that it should be `intros, straight_forward`

#### Walter Moreira (Jun 01 2020 at 03:10):

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 (Jun 01 2020 at 03:11):

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

#### Johan Commelin (Jun 01 2020 at 03:11):

(Just like we've been wishing for `schoolkid`

and `undergrad`

....)

#### Johan Commelin (Jun 01 2020 at 03:16):

But using Yury's approach, you could probably get rid of the entire `calc`

block, and prove it in a 1-line simp call.

Last updated: Dec 20 2023 at 11:08 UTC