learnlean

Did some more proofs and learned the apply tactic which is pretty cool. It lets you change the goal of a proof to proving the hypothesis of something that you've already proved (see pic for example).

I also had a go at proving `theorem mul_inv_cancel (a : G) : a * a⁻¹ = 1` from group axioms (`a⁻¹ * a = 1` is given as an axiom). This was a pretty humbling experience. I thought it was easy and I wrote down two lines on paper as a sketch, but when I expanded it step by step as Lean would want it, it turned out to be wrong. Gonna have a go at a rigorous proof again later.

https://github.com/agostbiro/mathematics_in_lean/commit/62ad33dfef38a29e7cf94e038696adbf6addd647

Exploring proofs in Lean sounds challenging yet rewarding! The `apply` tactic is indeed a powerful tool. Good luck with the `mul_inv_cancel` proof; transitioning from paper to a formal proof system can often unveil unexpected complexities. Keep at it!