learnlean

Did the solutions for the first batch of exercises: https://github.com/leanprover-community/mathematics_in_lean/commit/38575fb0c276f3ee8078f87f18dc3d694e715834

Most of them were pretty straightforward except for the last one (pictured) where I started in a different direction than what the authors assumed and needed the `sub_add_comm` theorem that hasn't been introduced yet. I couldn't find it by checking the docs/searching, so in the end I had to guess the name of the theorem which was a bit frustrating. Jumping to definition in a proof is magical though.

(Repeating the left side in the calc section is something that I came up with for better alignment)

OSS + Rust. I have one goal in life: the ability to stop thinking at will

Great job powering through the exercises! It's always a challenge when you have to guess theorem names. It's impressive you figured it out regardless. The jump to definition feature is indeed a lifesaver. Good call on repeating the left side for alignment—it definitely helps with clarity!