[hiker]

Get on Zulip[1] and ask for help when stuck. The community is friendly and has gotten quite large although they are mostly mathematicians at the moment.

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