Add Lean tactics as keywords

[jthulhu]

Currently, some tactics are syntax highlighted as keywords, and others are not. This PR makes every tactic that is documented in the Lean reference highlighted as a keyword, to be more consistent with semantic syntax highlighting.

[mekeor]

I opened the Lean Tactic Reference at https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/ with a webbrowser and executed the following snippet in the webbrowser Javascript console:

// Find all documentation entries:
Array.from(document.querySelectorAll("div.namedocs"))
  // Only consider entries documenting tactics:
  .filter(e => e.querySelector('span.label').innerText === "tactic")
  // Only consider the name of the tactic, not its description:
  .map(e => e.querySelector('pre.signature').innerText)
  // Don't consider tactics with complex syntax,
  // because it'd be a bigger task to highlight them correctly:
  .filter(signature => !signature.includes(" "))
  // Sort for better maintainability:
  .sort()

It yields this list:

[
  "ac_nf",
  "ac_nf0",
  "ac_rfl",
  "admit",
  "and_intros",
  "apply",
  "apply?",
  "apply_assumption",
  "apply_ext_theorem",
  "apply_mod_cast",
  "apply_rfl",
  "apply_rules",
  "as_aux_lemma",
  "assumption",
  "assumption_mod_cast",
  "bv_check",
  "bv_decide",
  "bv_decide?",
  "bv_normalize",
  "bv_omega",
  "by_cases",
  "calc",
  "cases",
  "change",
  "classical",
  "congr",
  "constructor",
  "contradiction",
  "dbg_trace",
  "decide",
  "decreasing_with",
  "delta",
  "done",
  "dsimp",
  "dsimp!",
  "dsimp?",
  "dsimp?!",
  "eq_refl",
  "erw",
  "exact",
  "exact?",
  "exact_mod_cast",
  "exfalso",
  "exists",
  "expose_names",
  "ext",
  "ext1",
  "false_or_by_contra",
  "fun_cases",
  "fun_induction",
  "funext",
  "generalize",
  "get_elem_tactic",
  "get_elem_tactic_trivial",
  "guard_expr",
  "guard_hyp",
  "guard_target",
  "induction",
  "infer_instance",
  "injection",
  "injections",
  "intro",
  "intros",
  "left",
  "native_decide",
  "nofun",
  "nomatch",
  "norm_cast",
  "obtain",
  "omega",
  "push_cast",
  "rcases",
  "refine",
  "refine'",
  "replace",
  "rewrite",
  "rfl",
  "rfl'",
  "right",
  "rintro",
  "run_tac",
  "rw",
  "rw?",
  "rw_mod_cast",
  "rwa",
  "show",
  "show_term",
  "simp",
  "simp!",
  "simp?",
  "simp?!",
  "simp_all",
  "simp_all!",
  "simp_all?",
  "simp_all?!",
  "simp_all_arith",
  "simp_all_arith!",
  "simp_arith",
  "simp_arith!",
  "simp_wf",
  "simpa",
  "simpa!",
  "simpa?",
  "simpa?!",
  "skip",
  "sleep",
  "solve",
  "solve_by_elim",
  "sorry",
  "specialize",
  "split",
  "stop",
  "subst",
  "subst_eqs",
  "subst_vars",
  "suffices",
  "symm",
  "symm_saturate",
  "trace",
  "trace_state",
  "trivial",
  "unfold",
  "unhygienic",
  "with_reducible",
  "with_reducible_and_instances",
  "with_unfolding_all"
]

In particular, it contains entries like with_reducible that are not part of your PR. Also, your PR adds entries like enter which my list does not contain.

How did you aggregate your list? Is there any clever way to tackle this problem with some sort of completeness expectation?