add one more to sum

Stream: new members

[Alex Kontorovich]

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]

sum_range_succ

[Patrick Massot]

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

[Alex Kontorovich]

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

[Patrick Massot]

Try replacing this sorry, by by library_search.

[PV]

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

[Kevin Buzzard]

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.

[PV]

ahh thanks.

[Bryan Gin-ge Chen]

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

Here it is in the mathlib tactic docs. See also suggest.