proof basics

Stream: maths

[Nicholas McConnell]

In proving the sum of two odd natural numbers is even, I got to this goal:

2 * k + 1 + (2 * l + 1) = 2 * k + 2 * l + 2 * 1

but am unsure how to go further. "ring" didn't work, and "simp" only got me to 1 + (1 + (2 * k + 2 * l)) = 2 + (2 * k + 2 * l), on which I can't seem to apply add_assoc. I also tried saying "import tactic" at the beginning and that didn't work.

[Rob Lewis]

ring will solve this. Do you have mathlib installed? If so, I think there's something wrong with your configuration, because import tactic should work.

[Nicholas McConnell]

I don't think I have mathlib; what's the best way to get it?

[Rob Lewis]

https://github.com/leanprover-community/mathlib#installation

[Nicholas McConnell]

Alright, thank you