Anton Kovsharov

Probably not fully resolving this, but [DiagnosticRelatedInformation](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#diagnosticRelatedInformation) can be useful to point to the underlying error. It's displayed in the hover message as the link which opens the related file...

Hi Heather, that's indeed an interesting example. **tldr;** Paperproof doesn't explicitly check tactic names and tries to be as generic as possible. However the heuristic we apply to prettify `have`-like...