docs: tactic writing tutorial

[arthurpaulino]

No description provided.

[EdAyers]

I can help with this!

[EdAyers]

Ok that's everything I've got. Feel free to edit or delete or restructure! Also a lot of todos that I will try to work through.

[digama0]

I think that the tutorial should be written in markdown with lean code blocks, instead of being a lean file with markdown blocks. That will also fix the build error.

[arthurpaulino]

@digama0 I talked to Edward and we're going to extract the tutorial content from this repo to avoid the mess of the process. Once the markdown files are ready I will let the community know and then we will be able to choose their destination. In the meantime, I intend to code in Lean to make sure everything typechecks and then convert those files to markdown using my lean2md.py script.