docstring の中で可換図式が書ける

Some thoughts:

• Infoview hovers already support MathJax, and MathJax supports AMScd. It's unfortunately a very limited package, but e.g. hovering on test below in the infoview shows a diagram

/--
$\begin{CD}
  A @>a>> B\\
  @V b V V= @VV c V\\
  C @>>d> D
\end{CD}$
-/
theorem test : True := ⟨⟩

#check id test

• Adding any visualization to hovers not in the infoview is an open problem (vscode-lean4#541).
• A PR adding support for other kinds of visualization, e.g. quiver diagram descriptions, to infoview hovers would probably be quite welcome. The community would have to come to some agreement on which format to use; quiver can parse tikz-cd code, so that might be a good solution.

Reproduce the provided Lean snippet and inspect how MathJax AMScd renders in an infoview hover. Read vscode-lean4#541 and investigate the proposed visualization formats, including quiver and tikz-cd; the work is complete only after the community agrees on a format and infoview support is implemented.