Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
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
0 reply
2 recasts
8 reactions
