## Stream: new members

### Topic: add one more to sum

#### Alex Kontorovich (Apr 10 2020 at 20:49):

Hi all, is there a tactic that just takes care of this? \sum_{i<n+1}a(i) = \sum_{i<n}a(i) + a(n) Thanks!

lemma sum_succ_is_add_last_term (a:ℕ→α )( n:ℕ ):
(sum (range (n+1)) a = sum (range n) a + a (n+1))
:=
sorry,


#### Kenny Lau (Apr 10 2020 at 20:50):

sum_range_succ

#### Patrick Massot (Apr 10 2020 at 20:52):

He asked for a tactic. The answer is thus library_search.

#### Alex Kontorovich (Apr 10 2020 at 20:54):

Perfect, thanks! (What is library_search? Something where I could've found this on my own?)

#### Patrick Massot (Apr 10 2020 at 20:55):

Try replacing this sorry, by by library_search.

#### PV (Apr 10 2020 at 22:24):

do you have to do anything special to make that work in the web viewer?

#### Kevin Buzzard (Apr 10 2020 at 22:28):

you have to use the right web viewer. The official Lean one has a very old mathlib. The one I link to has a bang up to date one, thanks to the amazing efforts of the leanprover-community people. Oh -- you also need to import tactic.

ahh thanks.

#### Bryan Gin-ge Chen (Apr 10 2020 at 22:48):

What is library_search? Something where I could've found this on my own?

Last updated: May 13 2021 at 18:26 UTC