tactic docs have unwieldy anchors for multiple tactics

[alexjbest]

On the tactics page some tactics have multiple names or are very similar left / right and by_contra / by_contradiction for one. So the links in the sidebar or by clicking on headings have spaces in them https://leanprover-community.github.io/mathlib_docs/tactics.html#nth_rewrite%20/%20nth_rewrite_lhs%20/%20nth_rewrite_rhs

This causes links like tactic#refl or tactic#left not to work on zulip which is a little sad.

[bryangingechen]

We could add a new field to the tactic doc entry structure to store a list of anchors, and then make doc-gen add all of those to the HTML.

[bryangingechen]

In fact, spaces are not even really allowed in id attributes: https://validator.w3.org/nu/?doc=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib_docs%2Ftactics.html

(This also affects the attributes, commands, hole_commands and notes pages.)

One simple fix for the spacing issue is to have doc-gen replace spaces with dashes, as it currently does for Markdown headings:

https://github.com/leanprover-community/doc-gen/blob/f6d8b3016f098f19d962f90f6dc03509c0969b65/mistletoe_renderer.py#L74-L77

It's probably still worthwhile to do something to get both tactic#left and tactic#right pointing to the right place though.