A motley collection of Corrections, Complaints and (Curious) Suggestions

[ghost]

Thanks for creating this, it was the most fun, accessible, and friendly introduction to lean I've encountered, including the various online books/tutorials I've tried.

Typos

• tactics/rw, "There are two distinct situations where use this tactics."
• W3L1 "those two results above are you've got right now. "
• W6L7: title "function world." should be "proposition world." (likely a copy-paste oversight)

Problem Spots

• W7L8: The postscript says "did you spot the import?", but it's actually marked as hidden, so no could spot it unless they look at the solution.
• W7L9 tauto is visibly imported but not discussed, nor does it appear in the tactics sidebar (until the next level W7L10).
• W3L5 gives tips on using repeat and rwa, but doesn't add them to the tactics tab in the side panel

Suggested Improvement

• W7L9: mentions the at form of rw, i.e. rw foo at h, for the first time, without explanation. rw is introduced and discussed at length in W1L2, but doesn't mention that rw can rewrite hypotheses, not just the goal. It is documented in the tactics sidebar, but is easy to miss. It is however used in the solutions quite early. My own experience was that I didn't realize this possibility until W7L9 included such a step without any explanation. I suggest that W1L2 should include a brief mention of this ability of rw.
• W2L6: Ater readin he postscript I was misled into thinking that the snippet

  instance : add_comm_monoid mynat := by structure_helper

  can be input into box, when in fact it belongs in the preamble, which isn't modifiable in the game (I don't think). I think this section would benefit from some tweaks.

• W2L6 (again): The postscript introduces "collectibles" as a friendly analogy for instances. I found it hard to understand what these are and what they do from the description. I also think that if simp is introduced in this level, it should be made clear when and where it is available within the game. Overall I think this section should be prefaced by a clear warning that:
  1. the code examples are intended for lean proper
  2. That the game includes them behind the scenes in later level (already mentioned), and what this means in principle (From what I gather... they supercharge simp when activated?)

Misc Nitpicks

• W7L8: no discussion here of the implicit parenthesis which lean places on logical connectives, unlike earlier discussions for arithmetic, and function types. The latex typeset lemma does clarify this (but that was also true for arithmetic and function types, and a discussion was included).
• W7L10: In "Instead of starting with all the intros, try this instead:" (intros gets typeset very like intros), so could instead be written " Instead of starting with several intro steps, try this instead:"
• W7L10: in postscript, tauto is actually enough to complete the proof, the difference between the two isn't explained, and it's surprising that an import of tauto makes tauto! available since in in all previous cases the import and tactic names matched exactly. A brief explanation like "the import makes both tauto and its extra-strength variant tauto! available" would have been nice.