tactic#interval_cases: syntax highlighting not working

[bryangingechen]

See https://leanprover-community.github.io/mathlib_docs/tactics.html#interval_cases

Not sure what's going on here, since the highlighting here works, and the relevant parts of the docstring markdown look the same to me: compare https://github.com/leanprover-community/mathlib/blob/d41f386/src/tactic/interval_cases.lean#L213 and line 249.

[gebner]

The obvious difference is that one is a docstring for a declaration, while the other is a docstring for a user command.

I would conjecture that the preprocessing step which replaces ``` by ```lean is only used for declaration docstrings.

As a fix, we could default to lean when highlighting markdown code blocks. This would require us to switch to the mistletoe renderer (used by the website), because it's hard to change the syntax highlighting in the markdown2 renderer.

[robertylewis]

Fixed by #110