feat: whitespace tactic completion & tactic completion docs

[mhuisi]

This PR enables tactic completion in the whitespace of a tactic proof and adds tactic docstrings to the completion menu.

Future work:

• A couple of broken tactic completions: This is due to tactic completion now using @david-christiansen's Tactic.Doc.allTacticDocs to obtain the tactic docstrings and should be fixed soon.
• Whitespace tactic completion in tactic combinators: This requires changing the syntax of tactic combinators to produce a syntax node that makes it clear that a tactic is expected at the given position.

Closes #1651.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-10-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-10-10 09:31:02)