Comment by aban

An Introduction to Lean [0] is another nice (albeit incomplete) tutorial.

There’s a fairly active community over on Zulip [1] if you like to drop by for a chat or get some help.

[0]: https://leanprover.github.io/introduction_to_lean/

[1]: https://leanprover.zulipchat.com