Markus Himmel

Incorrect highlighting if deprecation message contains `]` character

1

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

`rintro` error message is in the wrong place

1

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...

### Description While a file is still elaborating, expanded trace nodes in the info view are automatically closed. ### Steps to Reproduce See [video](https://www.youtube.com/watch?v=9h8EPsvkfNU). The file I used is available...

Define exact sequences

3

The usual definition of exactness in category theory seems to be along the lines of "the image of `f` is a kernel of `g`". I have found this definition to...

`interval_cases` for `pnat`s does not work, because `norm_num` does not support `pnat` (except sometimes)

4

The following fails (Lean 3.17.1): ```lean import tactic.interval_cases example (n : ℕ+) (h0 : 4 ≤ n) (h1 : 3 ≤ n) (h2 : n < 5) : n =...

### Prerequisites Please put an X between the brackets as you perform the following steps: * [x] Check that your issue is not already filed: https://github.com/leanprover/lean4/issues * [x] Reduce the...