Minimum Working Example (MWE)

A minimum working example is a code snippet that can be copied-and-pasted and still have the same features (working) and that does not include unnecessary details (minimum).

Here is the stackoverflow guide to making MWEs.

Please make sure that your code snippet has:

• correct imports; and
• all the relevant definitions / theorems.

(If your example comes from e.g. the Natural Number Game, then adding a link to the webpage works fine in lieu of finding the correct imports. So for example it would be much more useful to say "I am on this level of the Natural Number Game and my proof script is ", rather than "I am on Advanced Multiplication World Level 4 of the Natural Number Game and my proof script is ".)

In particular, you should test this by making a new Lean file, pasting your code snippet into it, and seeing if you get the expected behavior. This is exactly what people who try to help you will do!

If you post a code snippet on Zulip, please make sure it is surrounded in triple backticks.

```
def my_nat : nat := 5
```