I have to go now, so hopefully these short notes help!

Intro Level 1/4

As discussed: rw does a refl and rewrite does not.

Note the first word lemma is a keyword (highlighted in blue) and means we are stating a new lemma.

This is not blue for me. Maybe you need to enable syntax highlighting for the code snippets? I think you can write:

```lean
lemma add_comm : ∀ (x : ℕ) (y : ℕ), x + y = y + x
```

Intro Level 3/4

The following sequence of tactics causes a goal that the player cannot solve:

rewrite [hPQ]
rewrite [hQR]
rewrite [not_not]
rewrite [iff_self]
rewrite [iff_true]
rewrite [iff_self]

Maybe you can add a hint saying how to undo the last move (to do rfl instead)?

Intro Level 4/4

Should there be a note that P ∧ Q ∧ R = P ∧ (Q ∧ R)? Otherwise they might get confused why their rewrites are not working.