1) In the the "hard level", showing that multiplication by a positive number is injective, I needed to instantiate a forall statement for a particular value, but I couldn't figure out how to do _anything_ with a forall statement in the assumptions. I Googled that you can do this with "specialize", this was not a tactic explicitly allowed but it worked.
2) Maybe I have been doing things wrong, but many times I explicitly wrote "have a : 'some statement' := 'some reason'" where I explicitly used "0" in the statement. Looking at the error messages I figured out that "0" is interpreted as a nat rather than as a mynat, and through trial and error I figured out that I can write (0:mynat) to coerce.
3) It was impossible for me to figure out, in many situations, whether I should put in the implicit type arguments explicitly. I don't know if there is anything subtle there but I felt it's random and just did trial and error. There could be some well-placed words about when it occurs... E.g. in world 10 problem 13 I wrote
intro h,
cases h,
rw succ_add at h_h,
rw add_comm at h_h,
rw ← succ_add at h_h,
rw add_comm at h_h,
symmetry at h_h,
have t : (succ h_w) = 0 := eq_zero_of_add_right_eq_self a (succ h_w) h_h,
and then had to erase (a succ h_w) because it wasn't needed after all. Wait, is this because it sometimes says {...} and sometimes (...)?
4) Not so important, but sometimes "Proof complete!" takes a long time to appear after "no goals", and sometimes I forget to wait and then the level doesn't show up as passed.
5) Maybe this is more a comment about the interface of Lean than about the game, but often I want to write some complicated have statement, and I need to apply some specific lemma to some specific arguments. When I start writing that, I keep copying things from the top right box. Of course, before I get to the comma, its contents change. So I often need to copy things to a text editor or keep a lot of stuff in my head.