### Prerequisites

* [ ] Put an X between the brackets on this line if you have done all of the following:
    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean4/issues).
    * Reduced the issue to a self-contained, reproducible test case.

### Description

[Description of the issue]

### Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

**Expected behavior:** [What you expect to happen]

**Actual behavior:** [What actually happens]

**Reproduces how often:** [What percentage of the time does it reproduce?]

### Versions

You can get this information from copy and pasting the output of `lean --version`,
please include the OS and what version of the OS you're running.

### Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.
