Barry @chiroptical.dev · Oct 30 Finished Section 2.2 of Mathematics in Lean. I'm skeptical that anything beyond this will make sense... This was labeled a hard exercise, but my brain has no idea why I would introduce `h` as a goal to solve this. I feel like I need more raw math skills which probably isn't surprising to some.
6 likes 2 replies
Replies
group theory can indeed be unintuitive at times. it’s not as much about mathematical skill as it is about getting experience with how groups behave also, staring at a finished Lean proof is often not very helpful for figuring out how it was made. stepping through the intermediate states may help
Also, the apply syntax to re-write the current goal into a new goal is pretty confusing. If I have multiple named goals what does it re-write to?