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:

doc-gen/mistletoe_renderer.py

Lines 74 to 77 in f6d8b30

	# generate anchor following what github does
	# See info and links at https://gist.github.com/asabaylus/3071099
	anchor = inner.strip().lower()
	anchor = re.sub(r'[^\w\- ]+', '', anchor).replace(' ', '-')

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