Interleave Lean code with explanations

[david-christiansen]

It would be really useful to be able to interleave lines of Lean code (especially proof steps) with text that explains it.

Here's a design sketch. A multilean directive could gather and assemble all lean blocks under it, and elaborate the whole thing. It could look like this:

:::multilean
```lean
theorem five_eq_5' : a = 5 := by
  have : "a" = "a" := by rfl
```
Explain what `have` does
```lean
  rfl
```
:::

Challenges:

1. The process of rendering code to HTML is currently based on traversal of a syntax object. How do we split this? Perhaps render only those tokens in a certain source range?
2. How do we refer to individual scopes in the intervening code? It should be possible for the Explain ... line to contain references to local bindings in the preceding line, even in the presence of shadowing.

Another way that's less flexible but perhaps easier to get quality output from would be to have an "explanation" tactic that causes Verso's code renderer/elaborator to escape, such as:

theorem five_eq_5' : a = 5 := by
  have : "a" = "a" := by rfl
  explanation /-- Explain what `have` does -/
  rfl

This makes it easy to get the current scope, but it's perhaps somewhat less ergonomic.