diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 6b67701de9..2834a21553 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -518,14 +518,13 @@ syntax location := withPosition(ppGroup(" at" (locationWildcard <|> locationHyp)
   assuming these are definitionally equal.
 * `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
   assuming `t` and `t'` are definitionally equal.
--/
-syntax (name := change) "change " term (location)? : tactic
-
-/--
 * `change a with b` will change occurrences of `a` to `b` in the goal,
   assuming `a` and `b` are definitionally equal.
 * `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
 -/
+syntax (name := change) "change " term (location)? : tactic
+
+@[tactic_alt change]
 syntax (name := changeWith) "change " term " with " term (location)? : tactic
 
 /--
@@ -905,8 +904,13 @@ The tactic supports all the same syntax variants and options as the `let` term.
 -/
 macro "let" c:letConfig d:letDecl : tactic => `(tactic| refine_lift let $c:letConfig $d:letDecl; ?_)
 
-/-- `let rec f : t := e` adds a recursive definition `f` to the current goal.
-The syntax is the same as term-mode `let rec`. -/
+/--
+`let rec f : t := e` adds a recursive definition `f` to the current goal.
+The syntax is the same as term-mode `let rec`.
+
+The tactic supports all the same syntax variants and options as the `let` term.
+-/
+-- Uncomment after stage0 update: @[tactic_name "let rec"]
 syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic
 macro_rules
   | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_)
@@ -1212,22 +1216,6 @@ while `congr 2` produces the intended `⊢ x + y = y + x`.
 syntax (name := congr) "congr" (ppSpace num)? : tactic
 
 
-/--
-In tactic mode, `if h : t then tac1 else tac2` can be used as alternative syntax for:
-```
-by_cases h : t
-· tac1
-· tac2
-```
-It performs case distinction on `h : t` or `h : ¬t` and `tac1` and `tac2` are the subproofs.
-
-You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
-if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
-by the end of the block.
--/
-syntax (name := tacDepIfThenElse)
-  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
-    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
 /--
 In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
@@ -1236,16 +1224,34 @@ by_cases t
 · tac1
 · tac2
 ```
-It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous
-hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use
-nondependent `if`, since this wouldn't add anything to the context and hence would be
-useless for proving theorems. To actually insert an `ite` application use
-`refine if t then ?_ else ?_`.)
+It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and
+`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't
+add anything to the context and hence would be useless for proving theorems. To actually insert an
+`ite` application use `refine if t then ?_ else ?_`.)
+
+The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as
+alternative syntax for:
+```
+by_cases h : t
+· tac1
+· tac2
+```
+It performs case distinction on `h : t` or `h : ¬t`.
+
+You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
+if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
+by the end of the block.
 -/
 syntax (name := tacIfThenElse)
   ppRealGroup(ppRealFill(ppIndent("if " term " then") ppSpace matchRhsTacticSeq)
     ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
 
+
+@[tactic_alt tacIfThenElse]
+syntax (name := tacDepIfThenElse)
+  ppRealGroup(ppRealFill(ppIndent("if " binderIdent " : " term " then") ppSpace matchRhsTacticSeq)
+    ppDedent(ppSpace) ppRealFill("else " matchRhsTacticSeq)) : tactic
+
 /--
 The tactic `nofun` is shorthand for `exact nofun`: it introduces the assumptions, then performs an
 empty pattern match, closing the goal if the introduced pattern is impossible.
diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean
index 426b857437..db0575d024 100644
--- a/src/Lean/Elab/Tactic/Doc.lean
+++ b/src/Lean/Elab/Tactic/Doc.lean
@@ -8,6 +8,7 @@ module
 prelude
 import Lean.DocString
 public import Lean.Elab.Command
+public import Lean.Parser.Tactic.Doc
 
 public section
 
@@ -38,30 +39,42 @@ open Lean.Parser.Command
   | _ => throwError "Malformed 'register_tactic_tag' command"
 
 /--
-Gets the first string token in a parser description. For example, for a declaration like
-`syntax "squish " term " with " term : tactic`, it returns `some "squish "`, and for a declaration
-like `syntax tactic " <;;;> " tactic : tactic`, it returns `some " <;;;> "`.
-
-Returns `none` for syntax declarations that don't contain a string constant.
+Computes a table that heuristically maps parser syntax kinds to their first tokens by inspecting the
+Pratt parsing tables for the `tactic syntax kind. If a custom name is provided for the tactic, then
+it is returned instead.
 -/
-private partial def getFirstTk (e : Expr) : MetaM (Option String) := do
-  match (← Meta.whnf e).getAppFnArgs with
-  | (``ParserDescr.node, #[_, _, p]) => getFirstTk p
-  | (``ParserDescr.trailingNode, #[_, _, _, p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "withPosition")), p]) => getFirstTk p
-  | (``ParserDescr.unary, #[.app _ (.lit (.strVal "atomic")), p]) => getFirstTk p
-  | (``ParserDescr.binary, #[.app _ (.lit (.strVal "andthen")), p, _]) => getFirstTk p
-  | (``ParserDescr.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``ParserDescr.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | (``Parser.withAntiquot, #[_, p]) => getFirstTk p
-  | (``Parser.leadingNode, #[_, _, p]) => getFirstTk p
-  | (``HAndThen.hAndThen, #[_, _, _, _, p1, p2]) =>
-    if let some tk ← getFirstTk p1 then pure (some tk)
-    else getFirstTk (.app p2 (.const ``Unit.unit []))
-  | (``Parser.nonReservedSymbol, #[.lit (.strVal tk), _]) => pure (some tk)
-  | (``Parser.symbol, #[.lit (.strVal tk)]) => pure (some tk)
-  | _ => pure none
+def firstTacticTokens [Monad m] [MonadEnv m] : m (NameMap String) := do
+  let env ← getEnv
 
+  let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
+    | return {}
+
+  let mut firstTokens : NameMap String :=
+    tacticNameExt.toEnvExtension.getState env
+      |>.importedEntries
+      |>.push (tacticNameExt.exportEntriesFn env (tacticNameExt.getState env) .exported)
+      |>.foldl (init := {}) fun names inMods =>
+        inMods.foldl (init := names) fun names (k, n) =>
+          names.insert k n
+
+  firstTokens := addFirstTokens tactics tactics.tables.leadingTable firstTokens
+  firstTokens := addFirstTokens tactics tactics.tables.trailingTable firstTokens
+
+  return firstTokens
+where
+  addFirstTokens tactics table firsts : NameMap String := Id.run do
+    let mut firsts := firsts
+    for (tok, ps) in table do
+      -- Skip antiquotes
+      if tok == `«$» then continue
+      for (p, _) in ps do
+        for (k, ()) in p.info.collectKinds {} do
+          if tactics.kinds.contains k then
+            let tok := tok.toString (escape := false)
+            -- It's important here that the already-existing mapping is preserved, because it will
+            -- contain any user-provided custom name, and these shouldn't be overridden.
+            firsts := firsts.alter k (·.getD tok)
+    return firsts
 
 /--
 Creates some `MessageData` for a parser name.
@@ -71,18 +84,14 @@ identifiable leading token, then that token is shown. Otherwise, the underlying
 without an `@`. The name includes metadata that makes infoview hovers and the like work. This
 only works for global constants, as the local context is not included.
 -/
-private def showParserName (n : Name) : MetaM MessageData := do
+private def showParserName [Monad m] [MonadEnv m] (firsts : NameMap String) (n : Name) : m MessageData := do
   let env ← getEnv
   let params :=
     env.constants.find?' n |>.map (·.levelParams.map Level.param) |>.getD []
-  let tok ←
-    if let some descr := env.find? n |>.bind (·.value?) then
-      if let some tk ← getFirstTk descr then
-        pure <| Std.Format.text tk.trimAscii.copy
-      else pure <| format n
-    else pure <| format n
+
+  let tok := ((← customTacticName n) <|> firsts.get? n).map Std.Format.text |>.getD (format n)
   pure <| .ofFormatWithInfos {
-    fmt := "'" ++ .tag 0 tok ++ "'",
+    fmt := "`" ++ .tag 0 tok ++ "`",
     infos :=
       .ofList [(0, .ofTermInfo {
         lctx := .empty,
@@ -93,7 +102,6 @@ private def showParserName (n : Name) : MetaM MessageData := do
       })] _
   }
 
-
 /--
 Displays all available tactic tags, with documentation.
 -/
@@ -106,20 +114,22 @@ Displays all available tactic tags, with documentation.
     for (tac, tag) in arr do
       mapping := mapping.insert tag (mapping.getD tag {} |>.insert tac)
 
+  let firsts ← firstTacticTokens
+
   let showDocs : Option String → MessageData
     | none => .nil
     | some d => Format.line ++ MessageData.joinSep ((d.split '\n').map (toMessageData ∘ String.Slice.copy)).toList Format.line
 
-  let showTactics (tag : Name) : MetaM MessageData := do
+  let showTactics (tag : Name) : CommandElabM MessageData := do
     match mapping.find? tag with
     | none => pure .nil
     | some tacs =>
       if tacs.isEmpty then pure .nil
       else
         let tacs := tacs.toArray.qsort (·.toString < ·.toString) |>.toList
-        pure (Format.line ++ MessageData.joinSep (← tacs.mapM showParserName) ", ")
+        pure (Format.line ++ MessageData.joinSep (← tacs.mapM (showParserName firsts)) ", ")
 
-  let tagDescrs ← liftTermElabM <| (← allTagsWithInfo).mapM fun (name, userName, docs) => do
+  let tagDescrs ← (← allTagsWithInfo).mapM fun (name, userName, docs) => do
     pure <| m!"• " ++
       MessageData.nestD (m!"`{name}`" ++
         (if name.toString != userName then m!" — \"{userName}\"" else MessageData.nil) ++
@@ -146,13 +156,13 @@ structure TacticDoc where
   /-- Any docstring extensions that have been specified -/
   extensionDocs : Array String
 
-def allTacticDocs : MetaM (Array TacticDoc) := do
+def allTacticDocs (includeUnnamed : Bool := true) : MetaM (Array TacticDoc) := do
   let env ← getEnv
-  let all :=
-    tacticTagExt.toEnvExtension.getState (← getEnv)
-      |>.importedEntries |>.push (tacticTagExt.exportEntriesFn (← getEnv) (tacticTagExt.getState (← getEnv)) .exported)
+  let allTags :=
+    tacticTagExt.toEnvExtension.getState env |>.importedEntries
+      |>.push (tacticTagExt.exportEntriesFn env (tacticTagExt.getState env) .exported)
   let mut tacTags : NameMap NameSet := {}
-  for arr in all do
+  for arr in allTags do
     for (tac, tag) in arr do
       tacTags := tacTags.insert tac (tacTags.getD tac {} |>.insert tag)
 
@@ -160,15 +170,18 @@ def allTacticDocs : MetaM (Array TacticDoc) := do
 
   let some tactics := (Lean.Parser.parserExtension.getState env).categories.find? `tactic
     | return #[]
+
+  let firstTokens ← firstTacticTokens
+
   for (tac, _) in tactics.kinds do
     -- Skip noncanonical tactics
     if let some _ := alternativeOfTactic env tac then continue
-    let userName : String ←
-      if let some descr := env.find? tac |>.bind (·.value?) then
-        if let some tk ← getFirstTk descr then
-          pure tk.trimAscii.copy
-        else pure tac.toString
-      else pure tac.toString
+
+    let userName? : Option String := firstTokens.get? tac
+    let userName ←
+      if let some n := userName? then pure n
+      else if includeUnnamed then pure tac.toString
+      else continue
 
     docs := docs.push {
       internalName := tac,
diff --git a/src/Lean/Parser/Attr.lean b/src/Lean/Parser/Attr.lean
index f5cac7a9a4..5b170c3d4d 100644
--- a/src/Lean/Parser/Attr.lean
+++ b/src/Lean/Parser/Attr.lean
@@ -54,7 +54,7 @@ def externEntry := leading_parser
   nonReservedSymbol "extern" >> many (ppSpace >> externEntry)
 
 /--
-Declare this tactic to be an alias or alternative form of an existing tactic.
+Declares this tactic to be an alias or alternative form of an existing tactic.
 
 This has the following effects:
  * The alias relationship is saved
@@ -64,13 +64,26 @@ This has the following effects:
   "tactic_alt" >> ppSpace >> ident
 
 /--
-Add one or more tags to a tactic.
+Adds one or more tags to a tactic.
 
 Tags should be applied to the canonical names for tactics.
 -/
 @[builtin_attr_parser] def «tactic_tag» := leading_parser
   "tactic_tag" >> many1 (ppSpace >> ident)
 
+/--
+Sets the tactic's name.
+
+Ordinarily, tactic names are automatically set to the first token in the tactic's parser. If this
+process fails, or if the tactic's name should be multiple tokens (e.g. `let rec`), then this
+attribute can be used to provide a name.
+
+The tactic's name is used in documentation as well as in completion. Thus, the name should be a
+valid prefix of the tactic's syntax.
+-/
+@[builtin_attr_parser] def «tactic_name» := leading_parser
+  "tactic_name" >> ppSpace >> (ident <|> strLit)
+
 end Attr
 
 end Lean.Parser
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 0d9bfbd137..d9dc558100 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -52,24 +52,7 @@ example (n : Nat) : n = n := by
   optional Term.motive >> sepBy1 Term.matchDiscr ", " >>
   " with " >> ppDedent matchAlts
 
-/--
-The tactic
-```
-intro
-| pat1 => tac1
-| pat2 => tac2
-```
-is the same as:
-```
-intro x
-match x with
-| pat1 => tac1
-| pat2 => tac2
-```
-That is, `intro` can be followed by match arms and it introduces the values while
-doing a pattern match. This is equivalent to `fun` with match arms in term mode.
--/
-@[builtin_tactic_parser] def introMatch := leading_parser
+@[builtin_tactic_parser, tactic_alt intro] def introMatch := leading_parser
   nonReservedSymbol "intro" >> matchAlts
 
 builtin_initialize
diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean
index 214e6ac6a8..219f9e2eea 100644
--- a/src/Lean/Parser/Tactic/Doc.lean
+++ b/src/Lean/Parser/Tactic/Doc.lean
@@ -191,12 +191,13 @@ builtin_initialize
       unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind
       let `(«tactic_tag»|tactic_tag $tags*) := stx
         | throwError "Invalid `[{name}]` attribute syntax"
+
       if (← getEnv).find? decl |>.isSome then
         if !(isTactic (← getEnv) decl) then
-          throwErrorAt stx "`{decl}` is not a tactic"
+          throwErrorAt stx "`{.ofConstName decl}` is not a tactic"
 
       if let some tgt' := alternativeOfTactic (← getEnv) decl then
-        throwErrorAt stx "`{decl}` is an alternative form of `{tgt'}`"
+        throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`"
 
       for t in tags do
         let tagName := t.getId
@@ -271,14 +272,81 @@ where
     | [l] => " * " ++ l ++ "\n\n"
     | l::ls => " * " ++ l ++ "\n" ++ String.join (ls.map indentLine) ++ "\n\n"
 
+/--
+The mapping between tactics and their custom names.
+
+The first projection in each pair is the tactic name, and the second is the custom name.
+-/
+builtin_initialize tacticNameExt
+    : PersistentEnvExtension
+        (Name × String)
+        (Name × String)
+        (NameMap String) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {},
+    addImportedFn := fun _ => pure {},
+    addEntryFn := fun as (src, tgt) => as.insert src tgt,
+    exportEntriesFn := fun es =>
+      es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1)
+  }
+
+/--
+Finds the custom name assigned to `tac`, or returns `none` if there is no such custom name.
+-/
+def customTacticName [Monad m] [MonadEnv m] (tac : Name) : m (Option String) := do
+  let env ← getEnv
+  match env.getModuleIdxFor? tac with
+  | some modIdx =>
+    match (tacticNameExt.getModuleEntries env modIdx).binSearch (tac, default) (Name.quickLt ·.1 ·.1) with
+    | some (_, val) => return some val
+    | none => return none
+  | none => return tacticNameExt.getState env |>.find? tac
+
+builtin_initialize
+  let name := `tactic_name
+  registerBuiltinAttribute {
+    name := name,
+    ref := by exact decl_name%,
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwAttrMustBeGlobal name kind
+      let name ←
+        match stx with
+        | `(«tactic_name»|tactic_name $name:str) =>
+          pure name.getString
+        | `(«tactic_name»|tactic_name $name:ident) =>
+          pure (name.getId.toString (escape := false))
+        | _ => throwError "Invalid `[{name}]` attribute syntax"
+
+      if (← getEnv).find? decl |>.isSome then
+        if !(isTactic (← getEnv) decl) then
+          throwErrorAt stx m!"`{.ofConstName decl}` is not a tactic"
+        if let some idx := (← getEnv).getModuleIdxFor? decl then
+          if let some mod := (← getEnv).allImportedModuleNames[idx]? then
+            throwErrorAt stx m!"`{.ofConstName decl}` is defined in `{mod}`, but custom names can only be added in the tactic's defining module."
+          else
+            throwErrorAt stx m!"`{.ofConstName decl}` is defined in an imported module, but custom names can only be added in the tactic's defining module."
+
+      if let some tgt' := alternativeOfTactic (← getEnv) decl then
+        throwErrorAt stx "`{.ofConstName decl}` is an alternative form of `{.ofConstName tgt'}`"
+
+      if let some n ← customTacticName decl then
+        throwError m!"The tactic `{.ofConstName decl}` already has the custom name `{n}`"
+
+      modifyEnv fun env => tacticNameExt.addEntry env (decl, name)
+
+    descr :=
+      "Registers a custom name for a tactic. This custom name should be a prefix of the " ++
+      "tactic's syntax, because it is used in completion.",
+    applicationTime := .beforeElaboration
+  }
 
 -- Note: this error handler doesn't prevent all cases of non-tactics being added to the data
 -- structure. But the module will throw errors during elaboration, and there doesn't seem to be
 -- another way to implement this, because the category parser extension attribute runs *after* the
 -- attributes specified before a `syntax` command.
 /--
-Validates that a tactic alternative is actually a tactic and that syntax tagged as tactics are
-tactics.
+Validates that a tactic alternative is actually a tactic, that syntax tagged as tactics are
+tactics, and that syntax with tactic names are tactics.
 -/
 private def tacticDocsOnTactics : ParserAttributeHook where
   postAdd (catName declName : Name) (_builtIn : Bool) := do
@@ -291,6 +359,8 @@ private def tacticDocsOnTactics : ParserAttributeHook where
     if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then
       if !tags.isEmpty then
         throwError m!"`{.ofConstName declName}` is not a tactic"
+    if let some n := tacticNameExt.getState (← getEnv) |>.find? declName then
+      throwError m!"`{MessageData.ofConstName declName}` is not a tactic, but it was assigned a tactic name `{n}`"
 
 builtin_initialize
   registerParserAttributeHook tacticDocsOnTactics
diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean
index 64abd78e47..8dd5aa98da 100644
--- a/src/Lean/Server/Completion/CompletionCollectors.lean
+++ b/src/Lean/Server/Completion/CompletionCollectors.lean
@@ -597,7 +597,8 @@ def tacticCompletion
     (completionInfoPos : Nat)
     (ctx               : ContextInfo)
     : IO (Array ResolvableCompletionItem) := ctx.runMetaM .empty do
-  let allTacticDocs ← Tactic.Doc.allTacticDocs
+  -- Don't include tactics that are identified only by their internal parser name
+  let allTacticDocs ← Tactic.Doc.allTacticDocs (includeUnnamed := false)
   let items : Array ResolvableCompletionItem := allTacticDocs.map fun tacticDoc => {
       label          := tacticDoc.userName
       detail?        := none
diff --git a/src/Std/Tactic/Do/Syntax.lean b/src/Std/Tactic/Do/Syntax.lean
index 8aa67b6a41..1d8506cddf 100644
--- a/src/Std/Tactic/Do/Syntax.lean
+++ b/src/Std/Tactic/Do/Syntax.lean
@@ -290,6 +290,7 @@ syntax "∀" binderIdent : mintroPat
 @[tactic_alt Lean.Parser.Tactic.mintroMacro]
 syntax (name := mintro) "mintro" (ppSpace colGt mintroPat)+ : tactic
 
+@[tactic_alt Lean.Parser.Tactic.mintroMacro]
 macro (name := mintroError) "mintro" : tactic => Macro.throwError "`mintro` expects at least one pattern"
 
 macro_rules
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..bbc496d7e7 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,6 @@
 #include "util/options.h"
 
+// Dear CI, please update stage0
 namespace lean {
 options get_default_options() {
     options opts;
diff --git a/tests/lean/interactive/completionTactics.lean b/tests/lean/interactive/completionTactics.lean
index fed0331571..9477fdc7bc 100644
--- a/tests/lean/interactive/completionTactics.lean
+++ b/tests/lean/interactive/completionTactics.lean
@@ -118,3 +118,17 @@ example : True := by
   { skip -- All tactic completions expected
      }
   --^ completion
+
+/-!
+Now check that first token detection and tactic names work correctly in completion.
+-/
+
+/-- Local def -/
+syntax  "let " letDecl : tactic
+
+/-- Local recursive def -/
+@[tactic_name "let rec"]
+syntax (name := letrec) "let " &"rec" letRecDecls : tactic
+
+example : True := by
+                   --^ completion
diff --git a/tests/lean/interactive/completionTactics.lean.expected.out b/tests/lean/interactive/completionTactics.lean.expected.out
index ea6d6ac564..0e384f50d5 100644
--- a/tests/lean/interactive/completionTactics.lean.expected.out
+++ b/tests/lean/interactive/completionTactics.lean.expected.out
@@ -4,21 +4,21 @@
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 23, "character": 21}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -29,42 +29,35 @@
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -76,12 +69,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
 Resolution of exact:
@@ -89,32 +78,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 23, 21, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 26, "character": 24}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -125,42 +110,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}],
  "isIncomplete": false}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -172,12 +150,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
 Resolution of exact:
@@ -185,13 +159,9 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 26, 24, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 29, "character": 25}}
@@ -199,21 +169,21 @@ Resolution of Lean.Parser.Tactic.introMatch:
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 32, "character": 26}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -224,42 +194,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -271,12 +234,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
 Resolution of exact:
@@ -284,32 +243,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 32, 26, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 35, "character": 27}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -320,42 +275,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -367,12 +315,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
 Resolution of exact:
@@ -380,32 +324,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 35, 27, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 40, "character": 7}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -416,42 +356,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -463,12 +396,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
 Resolution of exact:
@@ -476,32 +405,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 40, 7, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 44, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -512,42 +437,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -559,12 +477,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
 Resolution of exact:
@@ -572,32 +486,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 44, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 49, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -608,42 +518,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -655,12 +558,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
 Resolution of exact:
@@ -668,32 +567,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 49, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 53, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -704,42 +599,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -751,12 +639,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
 Resolution of exact:
@@ -764,32 +648,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 53, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 59, "character": 4}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -800,42 +680,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -847,12 +720,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
 Resolution of exact:
@@ -860,32 +729,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 59, 4, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 64, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -896,42 +761,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -943,12 +801,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
 Resolution of exact:
@@ -956,32 +810,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 64, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 70, "character": 4}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -992,42 +842,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1039,12 +882,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
 Resolution of exact:
@@ -1052,32 +891,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 70, 4, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 76, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1088,42 +923,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1135,12 +963,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
 Resolution of exact:
@@ -1148,13 +972,9 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 76, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 81, "character": 4}}
@@ -1162,21 +982,21 @@ Resolution of Lean.Parser.Tactic.introMatch:
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 86, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1187,42 +1007,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1234,12 +1047,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
 Resolution of exact:
@@ -1247,32 +1056,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 86, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 91, "character": 4}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1283,42 +1088,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1330,12 +1128,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
 Resolution of exact:
@@ -1343,32 +1137,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 91, 4, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 96, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1379,42 +1169,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1426,12 +1209,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
 Resolution of exact:
@@ -1439,32 +1218,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 96, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 102, "character": 4}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1475,42 +1250,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1522,12 +1290,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
 Resolution of exact:
@@ -1535,13 +1299,9 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 102, 4, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 108, "character": 2}}
@@ -1549,21 +1309,21 @@ Resolution of Lean.Parser.Tactic.introMatch:
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 112, "character": 2}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1574,42 +1334,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1621,12 +1374,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
 Resolution of exact:
@@ -1634,32 +1383,28 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
  "kind": 14,
- "documentation":
- {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-  "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 112, 2, 0]}
 {"textDocument": {"uri": "file:///completionTactics.lean"},
  "position": {"line": 118, "character": 4}}
 {"items":
- [{"label": "Lean.Parser.Tactic.open",
+ [{"label": "open",
    "kind": 14,
    "documentation":
    {"value":
     "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
-  {"label": "Lean.Parser.Tactic.match",
+  {"label": "match",
    "kind": 14,
    "documentation":
    {"value":
     "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
     "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
-  {"label": "Lean.Parser.Tactic.set_option",
+  {"label": "set_option",
    "kind": 14,
    "documentation":
    {"value":
@@ -1670,42 +1415,35 @@ Resolution of Lean.Parser.Tactic.introMatch:
    "kind": 14,
    "documentation": {"value": "A docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
-  {"label": "Lean.Parser.Tactic.nestedTactic",
-   "kind": 14,
-   "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
-  {"label": "Lean.Parser.Tactic.unknown",
+  {"label": "ident",
    "kind": 14,
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
   {"label": "exact",
    "kind": 14,
    "documentation": {"value": "Another docstring ", "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]},
-  {"label": "Lean.Parser.Tactic.introMatch",
+  {"label": "intro",
    "kind": 14,
-   "documentation":
-   {"value":
-    "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
-    "kind": "markdown"},
    "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}],
  "isIncomplete": true}
-Resolution of Lean.Parser.Tactic.open:
-{"label": "Lean.Parser.Tactic.open",
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
   "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
-Resolution of Lean.Parser.Tactic.match:
-{"label": "Lean.Parser.Tactic.match",
+Resolution of match:
+{"label": "match",
  "kind": 14,
  "documentation":
  {"value":
   "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
   "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
-Resolution of Lean.Parser.Tactic.set_option:
-{"label": "Lean.Parser.Tactic.set_option",
+Resolution of set_option:
+{"label": "set_option",
  "kind": 14,
  "documentation":
  {"value":
@@ -1717,12 +1455,8 @@ Resolution of skip:
  "kind": 14,
  "documentation": {"value": "A docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
-Resolution of Lean.Parser.Tactic.nestedTactic:
-{"label": "Lean.Parser.Tactic.nestedTactic",
- "kind": 14,
- "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
-Resolution of Lean.Parser.Tactic.unknown:
-{"label": "Lean.Parser.Tactic.unknown",
+Resolution of ident:
+{"label": "ident",
  "kind": 14,
  "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
 Resolution of exact:
@@ -1730,11 +1464,106 @@ Resolution of exact:
  "kind": 14,
  "documentation": {"value": "Another docstring ", "kind": "markdown"},
  "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
-Resolution of Lean.Parser.Tactic.introMatch:
-{"label": "Lean.Parser.Tactic.introMatch",
+Resolution of intro:
+{"label": "intro",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 132, "character": 21}}
+{"items":
+ [{"label": "open",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "match",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "set_option",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ",
+    "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "ident",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "let rec",
+   "kind": 14,
+   "documentation": {"value": "Local recursive def ", "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "intro",
+   "kind": 14,
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]},
+  {"label": "let",
+   "kind": 14,
+   "documentation": {"value": "Local def ", "kind": "markdown"},
+   "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}],
+ "isIncomplete": true}
+Resolution of open:
+{"label": "open",
  "kind": 14,
  "documentation":
  {"value":
-  "The tactic\n```\nintro\n| pat1 => tac1\n| pat2 => tac2\n```\nis the same as:\n```\nintro x\nmatch x with\n| pat1 => tac1\n| pat2 => tac2\n```\nThat is, `intro` can be followed by match arms and it introduces the values while\ndoing a pattern match. This is equivalent to `fun` with match arms in term mode.\n",
+  "`open Foo in tacs` (the tactic) acts like `open Foo` at command level,\nbut it opens a namespace only within the tactics `tacs`. ",
   "kind": "markdown"},
- "data": ["«external:file:///completionTactics.lean»", 118, 4, 0]}
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of match:
+{"label": "match",
+ "kind": 14,
+ "documentation":
+ {"value":
+  "`match` performs case analysis on one or more expressions.\nSee [Induction and Recursion][tpil4].\nThe syntax for the `match` tactic is the same as term-mode `match`, except that\nthe match arms are tactics instead of expressions.\n```\nexample (n : Nat) : n = n := by\n  match n with\n  | 0 => rfl\n  | i+1 => simp\n```\n\n[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/induction_and_recursion.html\n",
+  "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of set_option:
+{"label": "set_option",
+ "kind": 14,
+ "documentation":
+ {"value":
+  "`set_option opt val in tacs` (the tactic) acts like `set_option opt val` at the command level,\nbut it sets the option only within the tactics `tacs`. ",
+  "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of skip:
+{"label": "skip",
+ "kind": 14,
+ "documentation": {"value": "A docstring ", "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of ident:
+{"label": "ident",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of let rec:
+{"label": "let rec",
+ "kind": 14,
+ "documentation": {"value": "Local recursive def ", "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of exact:
+{"label": "exact",
+ "kind": 14,
+ "documentation": {"value": "Another docstring ", "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of intro:
+{"label": "intro",
+ "kind": 14,
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
+Resolution of let:
+{"label": "let",
+ "kind": 14,
+ "documentation": {"value": "Local def ", "kind": "markdown"},
+ "data": ["«external:file:///completionTactics.lean»", 132, 21, 0]}
diff --git a/tests/lean/run/tacticDoc.lean b/tests/lean/run/tacticDoc.lean
index 081ad4fbdf..76c7e3515a 100644
--- a/tests/lean/run/tacticDoc.lean
+++ b/tests/lean/run/tacticDoc.lean
@@ -128,17 +128,78 @@ Note: This linter can be disabled with `set_option linter.tactic.docsOnAlt false
 attribute [tactic_alt my_trivial] «yetAnother»
 
 /-! # Querying Tactic Docs -/
+
+/-!
+`tm` is part of the below set because the tag attribute can't reject `someTerm` above before it is
+added. Because it's not a tactic, its first token is not found.
+-/
+
 /--
 info: Available tags: ⏎
   • `ctrl` — "control flow"
     Tactics that sequence or arrange other tactics ⏎
-    '<;>'
+    `<;>`
   • `extensible`
     Tactics that are intended to be extensible ⏎
-    'my_trivial'
+    `my_trivial`
   • `finishing`
     Finishing tactics that are intended to completely close a goal ⏎
-    'omega', 'my_trivial', 'someTerm'
+    `omega`, `my_trivial`, `tm`
 -/
 #guard_msgs in
 #print tactic tags
+
+/-!
+## Custom Names
+
+The next two tests check that custom tactic names are shown.
+-/
+@[tactic_tag finishing]
+syntax (name := fooBar) "foo" "bar" term : tactic
+
+
+/-!
+Here, the first token `foo` is shown:
+-/
+/--
+info: Available tags: ⏎
+  • `ctrl` — "control flow"
+    Tactics that sequence or arrange other tactics ⏎
+    `<;>`
+  • `extensible`
+    Tactics that are intended to be extensible ⏎
+    `my_trivial`
+  • `finishing`
+    Finishing tactics that are intended to completely close a goal ⏎
+    `omega`, `foo`, `my_trivial`, `tm`
+-/
+#guard_msgs in
+#print tactic tags
+
+attribute [tactic_name "foo bar"] fooBar
+
+/-!
+Now we show `foo bar`:
+-/
+/--
+info: Available tags: ⏎
+  • `ctrl` — "control flow"
+    Tactics that sequence or arrange other tactics ⏎
+    `<;>`
+  • `extensible`
+    Tactics that are intended to be extensible ⏎
+    `my_trivial`
+  • `finishing`
+    Finishing tactics that are intended to completely close a goal ⏎
+    `omega`, `foo bar`, `my_trivial`, `tm`
+-/
+#guard_msgs in
+#print tactic tags
+
+/-!
+This test checks that tactic names can't be added to other kinds of syntax.
+-/
+/-- error: `termNotATactic` is not a tactic, but it was assigned a tactic name `t` -/
+#guard_msgs in
+@[tactic_name t]
+syntax "not " "a " "tactic" : term
diff --git a/tests/lean/run/tacticDocAllModule.lean b/tests/lean/run/tacticDocAllModule.lean
new file mode 100644
index 0000000000..6257e28e6e
--- /dev/null
+++ b/tests/lean/run/tacticDocAllModule.lean
@@ -0,0 +1,25 @@
+module
+
+import Lean.Elab.Tactic.Doc
+
+/-!
+This test checks that the first tokens are found for the tactics that ship with Lean when in a
+module.
+
+In the past, the first token detection code attempted to process the descriptor in the environment;
+this failed in modules because the parser was not loaded. This test, along with tacticDocAllNonmod,
+check that the code works correctly both in and out of modules.
+-/
+
+open Lean.Elab.Tactic.Doc
+
+#guard_msgs in
+open Lean in
+#eval do
+  let docs ← allTacticDocs
+  let userNames := docs.map TacticDoc.userName
+  if userNames.size < 50 then
+    throwError "Implausibly few user names found: {userNames}"
+  for n in userNames do
+    if n.startsWith "Lean.Parser.Tactic" && n ≠ "Lean.Parser.Tactic.nestedTactic" then
+      logError "Didn't find a first token for tactic parser {n}"
diff --git a/tests/lean/run/tacticDocAllNonmod.lean b/tests/lean/run/tacticDocAllNonmod.lean
new file mode 100644
index 0000000000..804b80b5b4
--- /dev/null
+++ b/tests/lean/run/tacticDocAllNonmod.lean
@@ -0,0 +1,23 @@
+import Lean.Elab.Tactic.Doc
+
+/-!
+This test checks that the first tokens are found for the tactics that ship with Lean when not in a
+module.
+
+In the past, the first token detection code attempted to process the descriptor in the environment;
+this failed in modules because the parser was not loaded. This test, along with tacticDocAllModule,
+check that the code works correctly both in and out of modules.
+-/
+
+open Lean.Elab.Tactic.Doc
+
+#guard_msgs in
+open Lean in
+#eval do
+  let docs ← allTacticDocs
+  let userNames := docs.map TacticDoc.userName
+  if userNames.size < 50 then
+    throwError "Implausibly few user names found: {userNames}"
+  for n in userNames do
+    if n.startsWith "Lean.Parser.Tactic" && n ≠ "Lean.Parser.Tactic.nestedTactic" then
+      logError "Didn't find a first token for tactic parser {n}"
diff --git a/tests/lean/run/tacticDocUserName.lean b/tests/lean/run/tacticDocUserName.lean
new file mode 100644
index 0000000000..682ac402e7
--- /dev/null
+++ b/tests/lean/run/tacticDocUserName.lean
@@ -0,0 +1,61 @@
+import Lean
+
+open Lean Elab Tactic Doc
+
+/-!
+This test ensures that user-facing tactic names shipped with Lean are kept unambiguous.
+-/
+#eval show MetaM Unit from do
+  let firsts ← firstTacticTokens
+
+  -- Compute a reverse mapping from first tokens to their syntax kinds
+  let mut rev : Std.HashMap String (List Name) := {}
+  for (k, firstTok) in firsts do
+    rev := rev.alter firstTok fun x? => x?.map (k :: ·) |>.getD [k]
+
+  -- Check each for ambiguity
+  for (firstTok, kindsForToken) in rev do
+
+    -- Skip kinds that are alternative syntax for some user-facing parser
+    let kindsForToken ← kindsForToken.filterM fun k => do
+      pure <| (Parser.Tactic.Doc.alternativeOfTactic (← getEnv) k).isNone
+
+    -- Until a stage0 update allows let rec to have a custom name, ignore it. Then update this test.
+    let kindsForToken := kindsForToken.filter (· ≠ ``Lean.Parser.Tactic.letrec)
+    if firstTok.contains ' ' then throwError "Test needs updating after stage0 update (see comment)"
+
+    -- If it's ambiguous, log an error.
+    if kindsForToken.length > 1 then
+      let kinds := MessageData.andList <| kindsForToken.map (m!"`{.ofConstName ·}`")
+      logError m!"`{firstTok}` is the ambiguous first token for {kinds}"
+
+/-!
+This test ensures that user-facing tactic names are found for all the tactics that we ship.
+-/
+#eval show MetaM Unit from do
+  let firsts ← firstTacticTokens
+  let some tactics := (Lean.Parser.parserExtension.getState (← getEnv)).categories.find? `tactic
+    | return
+  for (t, ()) in tactics.kinds do
+    if t == ``Lean.Parser.Tactic.nestedTactic then continue
+    unless firsts.contains t do
+      logError m!"Couldn't find the first token for tactic syntax kind {t}"
+
+/-!
+This test spot-checks tactics defined in a few ways to make sure they all have user-facing names:
+ * Defined using `syntax ... : tactic`, both leading and trailing (`intros` and `<;>`)
+ * Defined using `declare_simp_like_tactic` (`simpAutoUnfold`)
+ * Defined with custom user-facing names (`Lean.Parser.Tactic.letrec`) (after stage0 update)
+-/
+/--
+info: (some intro)
+(some <;>)
+(some simp!)
+-/
+#guard_msgs in
+#eval show MetaM Unit from do
+  let firsts ← firstTacticTokens
+  IO.println (firsts.get? ``Lean.Parser.Tactic.intro)
+  IO.println (firsts.get? ``Lean.Parser.Tactic.«tactic_<;>_»)
+  IO.println (firsts.get? ``Lean.Parser.Tactic.simpAutoUnfold)
+  --IO.println (firsts.get? ``Lean.Parser.Tactic.letrec)