[Bug] [Lean] Editing after #doc in technical details ends up in the wrong block

[pimotte]

What happened?

When editing a Lean-based exercise file, edits after #doc end up going to markdown instead of codecells.

How can we reproduce this issue?

Example:

1. Open any Lean-based exercise sheet
2. Unfold the Technical details section at the top
3. Set the cursor at the end of the doc line
4. Type enter and text
5. Close and open the document.
6. Find that the text is in a markdown cell.

What was supposed to happen?

Either the text should end in a code cell or the edit should not be allowed in the first place.

I think this is kind of a niche occurrence and teachers likely won't be doing this to begin with. I'm good with either of these solutions, but not allowing the edit seems more robust. If we allow the edit, it will still be hard to keep the document consistent between editor and disk.

[pimotte]

Solution: modify the special casing of the Lean preamble to exclude display of the #doc line.