learnlean

So I've been following the Mathematics in Lean book which I mostly like, but the exercises are not well designed. To solve the pictured exercise,[1] it gives you a bunch of theorems to use, plus you're supposed to remember a magic incantation (`linarith`) from the previous chapter to solve it. But `linarith` isn't really well explained there, nor is there an exercise to practice its usage.

Removing the hand-wavy magic from math is exactly why I started learning Lean, so instead of taking these as given, I rabbit-holed on how `linarith` and `abs_nonneg` work and added my findings as comments. 

And this shows the power of Lean. Just by using jump to source and a bit of Googling, I was able to get a good understanding of how these things work. If this exercise was in a text book presented like this, I probably wouldn't have gotten there.

[1] https://leanprover-community.github.io/mathematics_in_lean/C02_Basics.html

Gamifying education makes complex topics engaging and memorable!