diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
index e2fa0e70d716..02a189bb28bb 100644
--- a/src/Lean/Elab/InfoTree/Types.lean
+++ b/src/Lean/Elab/InfoTree/Types.lean
@@ -83,7 +83,7 @@ inductive CompletionInfo where
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
-  | tactic (stx : Syntax) (goals : List MVarId)
+  | tactic (stx : Syntax)
   -- TODO `import`
 
 /-- Info for an option reference (e.g. in `set_option`). -/
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 00ccb76719c1..65acc4190782 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -313,7 +313,7 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 @[builtin_tactic skip] def evalSkip : Tactic := fun _ => pure ()
 
 @[builtin_tactic unknown] def evalUnknown : Tactic := fun stx => do
-  addCompletionInfo <| CompletionInfo.tactic stx (← getGoals)
+  addCompletionInfo <| CompletionInfo.tactic stx
 
 @[builtin_tactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx =>
   Term.withoutErrToSorry <| withoutRecover do
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index cde43a624c89..b4be29e8fe80 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -13,6 +13,7 @@ import Lean.Data.Lsp.Utf16
 import Lean.Meta.CompletionName
 import Lean.Meta.Tactic.Apply
 import Lean.Meta.Match.MatcherInfo
+import Lean.Elab.Tactic.Doc
 import Lean.Server.InfoUtils
 import Lean.Parser.Extension
 import Lean.Server.FileSource
@@ -651,100 +652,279 @@ private def optionCompletion
              data? := toJson { params, id? := none : CompletionItemDataWithId } }, score)
     return some { items := sortCompletionItems items, isIncomplete := true }
 
-private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : IO (Option CompletionList) :=
-  -- Just return the list of tactics for now.
-  ctx.runMetaM {} do
-    let table := Parser.getCategory (Parser.parserExtension.getState (← getEnv)).categories `tactic |>.get!.tables.leadingTable
-    let items : Array (CompletionItem × Float) := table.fold (init := #[]) fun items tk _ =>
-      -- TODO pretty print tactic syntax
-      items.push ({
-        label          := tk.toString
-        detail?        := none
-        documentation? := none
-        kind?          := CompletionItemKind.keyword
-        data?          := toJson { params, id? := none : CompletionItemDataWithId }
-      }, 1)
-    return some { items := sortCompletionItems items, isIncomplete := true }
+private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo)
+    : IO (Option CompletionList) := ctx.runMetaM .empty do
+  let allTacticDocs ← Tactic.Doc.allTacticDocs
+  let items : Array (CompletionItem × Float) := allTacticDocs.map fun tacticDoc =>
+    ({
+      label          := tacticDoc.userName
+      detail?        := none
+      documentation? := tacticDoc.docString.map fun docString =>
+        { value := docString, kind := MarkupKind.markdown : MarkupContent }
+      kind?          := CompletionItemKind.keyword
+      data?          := toJson { params, id? := none : CompletionItemDataWithId }
+    }, 1)
+  return some { items := sortCompletionItems items, isIncomplete := true }
 
-/--
-If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`,
-yields the closest one of those `Info`s.
-Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`.
--/
-private def findClosestInfoWithLocalContextAt?
-    (hoverPos : String.Pos)
+private def findBest?
     (infoTree : InfoTree)
-    : Option (ContextInfo × Info) :=
+    (gt : α → α → Bool)
+    (f : ContextInfo → Info → PersistentArray InfoTree → Option α)
+    : Option α :=
   infoTree.visitM (m := Id) (postNode := choose) |>.join
 where
   choose
       (ctx : ContextInfo)
       (info : Info)
-      (_ : PersistentArray InfoTree)
-      (childValues : List (Option (Option (ContextInfo × Info))))
-      : Option (ContextInfo × Info) :=
+      (cs : PersistentArray InfoTree)
+      (childValues : List (Option (Option α)))
+      : Option α :=
     let bestChildValue := childValues.map (·.join) |>.foldl (init := none) fun v best =>
       if isBetter v best then
         v
       else
         best
-    if info.occursInOrOnBoundary hoverPos && isBetter (ctx, info) bestChildValue then
-      (ctx, info)
+    if let some v := f ctx info cs then
+      if isBetter v bestChildValue then
+        v
+      else
+        bestChildValue
     else
       bestChildValue
-
-  isBetter (a b : Option (ContextInfo × Info)) : Bool :=
+  isBetter (a b : Option α) : Bool :=
     match a, b with
     | none,   none   => false
     | some _, none   => true
     | none,   some _ => false
-    | some (_, ia), some (_, ib) =>
-      if !ia.lctx.isEmpty && ib.lctx.isEmpty then
-        true
-      else if ia.lctx.isEmpty && !ib.lctx.isEmpty then
-        false
-      else if ia.isSmaller ib then
-        true
-      else if ib.isSmaller ia then
-        false
-      else
-        false
+    | some a, some b => gt a b
+
+/--
+If there are `Info`s that contain `hoverPos` and have a nonempty `LocalContext`,
+yields the closest one of those `Info`s.
+Otherwise, yields the closest `Info` that contains `hoverPos` and has an empty `LocalContext`.
+-/
+private def findClosestInfoWithLocalContextAt?
+    (hoverPos : String.Pos)
+    (infoTree : InfoTree)
+    : Option (ContextInfo × Info) :=
+  findBest? infoTree isBetter fun ctx info _ =>
+    if info.occursInOrOnBoundary hoverPos then
+      (ctx, info)
+    else
+      none
+where
+  isBetter (a b : ContextInfo × Info) : Bool :=
+    let (_, ia) := a
+    let (_, ib) := b
+    if !ia.lctx.isEmpty && ib.lctx.isEmpty then
+      true
+    else if ia.lctx.isEmpty && !ib.lctx.isEmpty then
+      false
+    else if ia.isSmaller ib then
+      true
+    else if ib.isSmaller ia then
+      false
+    else
+      false
+
+private def findSyntheticIdentifierCompletion?
+    (hoverPos : String.Pos)
+    (infoTree : InfoTree)
+    : Option (HoverInfo × ContextInfo × CompletionInfo) := do
+  let some (ctx, info) := findClosestInfoWithLocalContextAt? hoverPos infoTree
+    | none
+  let some stack := info.stx.findStack? (·.getRange?.any (·.contains hoverPos (includeStop := true)))
+    | none
+  let stack := stack.dropWhile fun (stx, _) => !(stx matches `($_:ident) || stx matches `($_:ident.))
+  let some (stx, _) := stack.head?
+    | none
+  let isDotIdCompletion := stack.any fun (stx, _) => stx matches `(.$_:ident)
+  if isDotIdCompletion then
+    -- An identifier completion is never useful in a dotId completion context.
+    none
+  let some (id, danglingDot) :=
+      match stx with
+      | `($id:ident) => some (id.getId, false)
+      | `($id:ident.) => some (id.getId, true)
+      | _ => none
+    | none
+  let tailPos := stx.getTailPos?.get!
+  let hoverInfo :=
+    if hoverPos < tailPos then
+      HoverInfo.inside (tailPos - hoverPos).byteIdx
+    else
+      HoverInfo.after
+  some (hoverInfo, ctx, .id stx id danglingDot info.lctx none)
+
+private partial def getIndentationAmount (fileMap : FileMap) (line : Nat) : Nat := Id.run do
+  let lineStartPos := fileMap.lineStart line
+  let lineEndPos := fileMap.lineStart (line + 1)
+  let mut it : String.Iterator := ⟨fileMap.source, lineStartPos⟩
+  let mut indentationAmount := 0
+  while it.pos < lineEndPos do
+    let c := it.curr
+    if c = ' ' || c = '\t' then
+      indentationAmount := indentationAmount + 1
+    else
+      break
+    it := it.next
+  return indentationAmount
+
+private partial def isSyntheticTacticCompletion
+    (fileMap  : FileMap)
+    (hoverPos : String.Pos)
+    (cmdStx   : Syntax)
+    : Bool := Id.run do
+  let hoverFilePos := fileMap.toPosition hoverPos
+  let mut hoverLineIndentation := getIndentationAmount fileMap hoverFilePos.line
+  if hoverFilePos.column < hoverLineIndentation then
+    -- Ignore trailing whitespace after the cursor
+    hoverLineIndentation := hoverFilePos.column
+  go hoverFilePos hoverLineIndentation cmdStx 0
+where
+  go
+      (hoverFilePos : Position)
+      (hoverLineIndentation : Nat)
+      (stx : Syntax)
+      (leadingWs : Nat)
+      : Bool := Id.run do
+    match stx.getPos?, stx.getTailPos? with
+    | some startPos, some endPos =>
+      let isCursorInCompletionRange :=
+        startPos.byteIdx - leadingWs <= hoverPos.byteIdx
+          && hoverPos.byteIdx <= endPos.byteIdx + stx.getTrailingSize
+      if ! isCursorInCompletionRange then
+        return false
+      let mut wsBeforeArg := leadingWs
+      for arg in stx.getArgs do
+        if go hoverFilePos hoverLineIndentation arg wsBeforeArg then
+          return true
+        -- We must account for the whitespace before an argument because the syntax nodes we use
+        -- to identify tactic blocks only start *after* the whitespace following a `by`, and we
+        -- want to provide tactic completions in that whitespace as well.
+        -- This method of computing whitespace assumes that there are no syntax nodes without tokens
+        -- after `by` and before the first proper tactic syntax.
+        wsBeforeArg := arg.getTrailingSize
+      return isCompletionInEmptyTacticBlock stx
+        || isCompletionAfterSemicolon stx
+        || isCompletionOnTacticBlockIndentation hoverFilePos hoverLineIndentation stx
+    | _, _ =>
+      -- Empty tactic blocks typically lack ranges since they do not contain any tokens.
+      -- We do not perform more precise range checking in this case because we assume that empty
+      -- tactic blocks always occur within other syntax with ranges that let us narrow down the
+      -- search to the degree that we can be sure that the cursor is indeed in this empty tactic
+      -- block.
+      return isCompletionInEmptyTacticBlock stx
+
+  isCompletionOnTacticBlockIndentation
+      (hoverFilePos : Position)
+      (hoverLineIndentation : Nat)
+      (stx : Syntax)
+      : Bool := Id.run do
+    let isCursorInIndentation := hoverFilePos.column <= hoverLineIndentation
+    if ! isCursorInIndentation then
+      -- Do not trigger tactic completion at the end of a properly indented tactic block line since
+      -- that line might already have entered term mode by that point.
+      return false
+    let some tacticsNode := getTacticsNode? stx
+      | return false
+    let some firstTacticPos := tacticsNode.getPos?
+      | return false
+    let firstTacticLine := fileMap.toPosition firstTacticPos |>.line
+    let firstTacticIndentation := getIndentationAmount fileMap firstTacticLine
+    -- This ensures that we do not accidentally provide tactic completions in a term mode proof -
+    -- tactic completions are only provided at the same indentation level as the other tactics in
+    -- that tactic block.
+    let isCursorInTacticBlock := hoverLineIndentation == firstTacticIndentation
+    return isCursorInProperWhitespace && isCursorInTacticBlock
+
+  isCompletionAfterSemicolon (stx : Syntax) : Bool := Id.run do
+    let some tacticsNode := getTacticsNode? stx
+      | return false
+    let tactics := tacticsNode.getArgs
+    -- We want to provide completions in the case of `skip;<CURSOR>`, so the cursor must only be on
+    -- whitespace, not in proper whitespace.
+    return isCursorOnWhitspace && tactics.any fun tactic => Id.run do
+      let some tailPos := tactic.getTailPos?
+        | return false
+      let isCursorAfterSemicolon :=
+        tactic.isToken ";"
+          && tailPos.byteIdx <= hoverPos.byteIdx
+          && hoverPos.byteIdx <= tailPos.byteIdx + tactic.getTrailingSize
+      return isCursorAfterSemicolon
+
+  getTacticsNode? (stx : Syntax) : Option Syntax :=
+    if stx.getKind == `Lean.Parser.Tactic.tacticSeq1Indented then
+      some stx[0]
+    else if stx.getKind == `Lean.Parser.Tactic.tacticSeqBracketed then
+      some stx[1]
+    else
+      none
+
+  isCompletionInEmptyTacticBlock (stx : Syntax) : Bool :=
+    isCursorInProperWhitespace && isEmptyTacticBlock stx
+
+  isCursorOnWhitspace : Bool :=
+    fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace
+
+  isCursorInProperWhitespace : Bool :=
+    (fileMap.source.atEnd hoverPos || (fileMap.source.get hoverPos).isWhitespace)
+      && (fileMap.source.get (hoverPos - ⟨1⟩)).isWhitespace
+
+  isEmptyTacticBlock (stx : Syntax) : Bool :=
+    stx.getKind == `Lean.Parser.Tactic.tacticSeq && isEmpty stx
+      || stx.getKind == `Lean.Parser.Tactic.tacticSeq1Indented && isEmpty stx
+      || stx.getKind == `Lean.Parser.Tactic.tacticSeqBracketed && isEmpty stx[1]
+
+  isEmpty : Syntax → Bool
+    | .missing       => true
+    | .ident ..      => false
+    | .atom ..       => false
+    | .node _ _ args => args.all isEmpty
+
+private partial def findOutermostContextInfo? (i : InfoTree) : Option ContextInfo :=
+  go i
+where
+  go (i : InfoTree) : Option ContextInfo := do
+    match i with
+  | .context ctx i =>
+    match ctx with
+    | .commandCtx ctxInfo =>
+      some { ctxInfo with }
+    | _ =>
+      -- This shouldn't happen (see the `PartialContextInfo` docstring),
+      -- but let's continue searching regardless
+      go i
+  | .node _ cs =>
+    cs.findSome? go
+  | .hole .. =>
+    none
+
+private def findSyntheticTacticCompletion?
+    (fileMap  : FileMap)
+    (hoverPos : String.Pos)
+    (cmdStx   : Syntax)
+    (infoTree : InfoTree)
+    : Option (HoverInfo × ContextInfo × CompletionInfo) := do
+  let ctx ← findOutermostContextInfo? infoTree
+  if ! isSyntheticTacticCompletion fileMap hoverPos cmdStx then
+    none
+  -- Neither `HoverInfo` nor the syntax in `.tactic` are important for tactic completion.
+  return (HoverInfo.after, ctx, .tactic .missing)
 
 private def findCompletionInfoAt?
     (fileMap  : FileMap)
     (hoverPos : String.Pos)
+    (cmdStx   : Syntax)
     (infoTree : InfoTree)
     : Option (HoverInfo × ContextInfo × CompletionInfo) :=
   let ⟨hoverLine, _⟩ := fileMap.toPosition hoverPos
   match infoTree.foldInfo (init := none) (choose hoverLine) with
   | some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
     some (hoverInfo, ctx, info)
-  | _ => do
-    -- No completion info => Attempt providing identifier completions
-    let some (ctx, info) := findClosestInfoWithLocalContextAt? hoverPos infoTree
-      | none
-    let some stack := info.stx.findStack? (·.getRange?.any (·.contains hoverPos (includeStop := true)))
-      | none
-    let stack := stack.dropWhile fun (stx, _) => !(stx matches `($_:ident) || stx matches `($_:ident.))
-    let some (stx, _) := stack.head?
-      | none
-    let isDotIdCompletion := stack.any fun (stx, _) => stx matches `(.$_:ident)
-    if isDotIdCompletion then
-      -- An identifier completion is never useful in a dotId completion context.
-      none
-    let some (id, danglingDot) :=
-        match stx with
-        | `($id:ident) => some (id.getId, false)
-        | `($id:ident.) => some (id.getId, true)
-        | _ => none
-      | none
-    let tailPos := stx.getTailPos?.get!
-    let hoverInfo :=
-      if hoverPos < tailPos then
-        HoverInfo.inside (tailPos - hoverPos).byteIdx
-      else
-        HoverInfo.after
-    some (hoverInfo, ctx, .id stx id danglingDot info.lctx none)
+  | _ =>
+    findSyntheticTacticCompletion? fileMap hoverPos cmdStx infoTree <|>
+      findSyntheticIdentifierCompletion? hoverPos infoTree
 where
   choose
       (hoverLine : Nat)
@@ -817,10 +997,11 @@ partial def find?
     (params   : CompletionParams)
     (fileMap  : FileMap)
     (hoverPos : String.Pos)
+    (cmdStx   : Syntax)
     (infoTree : InfoTree)
     (caps     : ClientCapabilities)
     : IO (Option CompletionList) := do
-  let some (hoverInfo, ctx, info) := findCompletionInfoAt? fileMap hoverPos infoTree
+  let some (hoverInfo, ctx, info) := findCompletionInfoAt? fileMap hoverPos cmdStx infoTree
     | return none
   let completionList? ←
     match info with
@@ -846,11 +1027,12 @@ in the context found at `hoverPos` in `infoTree`.
 def resolveCompletionItem?
     (fileMap  : FileMap)
     (hoverPos : String.Pos)
+    (cmdStx   : Syntax)
     (infoTree : InfoTree)
     (item     : CompletionItem)
     (id       : CompletionIdentifier)
     : IO CompletionItem := do
-  let some (_, ctx, info) := findCompletionInfoAt? fileMap hoverPos infoTree
+  let some (_, ctx, info) := findCompletionInfoAt? fileMap hoverPos cmdStx infoTree
     | return item
   ctx.runMetaM info.lctx (item.resolve id)
 
diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 493315eb4d0d..57418b4fa1cf 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -28,14 +28,14 @@ open Snapshots
 
 open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString)
 
-def findCompletionInfoTreeAtPos
+def findCompletionCmdDataAtPos
     (doc : EditableDocument)
     (pos : String.Pos)
-    : Task (Option Elab.InfoTree) :=
-  -- NOTE: use `+ 1` since we sometimes want to consider invalid input technically after the command,
-  -- such as a trailing dot after an option name. This shouldn't be a problem since any subsequent
-  -- snapshot that is eligible for completion should be separated by some delimiter.
-  findInfoTreeAtPos doc (fun s => s.data.stx.getTailPos?.any (· + ⟨1⟩ >= pos)) pos
+    : Task (Option (Syntax × Elab.InfoTree)) :=
+  findCmdDataAtPos doc (pos := pos) fun s => Id.run do
+    let some tailPos := s.data.stx.getTailPos?
+      | return false
+    return pos.byteIdx <= tailPos.byteIdx + s.data.stx.getTrailingSize
 
 def handleCompletion (p : CompletionParams)
     : RequestM (RequestTask CompletionList) := do
@@ -43,11 +43,11 @@ def handleCompletion (p : CompletionParams)
   let text := doc.meta.text
   let pos := text.lspPosToUtf8Pos p.position
   let caps := (← read).initParams.capabilities
-  mapTask (findCompletionInfoTreeAtPos doc pos) fun infoTree? => do
-    let some infoTree := infoTree?
+  mapTask (findCompletionCmdDataAtPos doc pos) fun cmdData? => do
+    let some (cmdStx, infoTree) := cmdData?
       -- work around https://github.com/microsoft/vscode/issues/155738
       | return { items := #[{label := "-"}], isIncomplete := true }
-    if let some r ← Completion.find? p doc.meta.text pos infoTree caps then
+    if let some r ← Completion.find? p doc.meta.text pos cmdStx infoTree caps then
       return r
     return { items := #[ ], isIncomplete := true }
 
@@ -67,10 +67,10 @@ def handleCompletionItemResolve (item : CompletionItem)
   let some id := data.id?
     | return .pure item
   let pos := text.lspPosToUtf8Pos data.params.position
-  mapTask (findCompletionInfoTreeAtPos doc pos) fun infoTree? => do
-    let some infoTree := infoTree?
+  mapTask (findCompletionCmdDataAtPos doc pos) fun cmdData? => do
+    let some (cmdStx, infoTree) := cmdData?
       | return item
-    Completion.resolveCompletionItem? text pos infoTree item id
+    Completion.resolveCompletionItem? text pos cmdStx infoTree item id
 
 open Elab in
 def handleHover (p : HoverParams)
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 8a850b1ac12f..5596982f976e 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -172,11 +172,6 @@ def Info.isSmaller (i₁ i₂ : Info) : Bool :=
   | some _, none => true
   | _, _ => false
 
-def Info.occursDirectlyBefore (i : Info) (hoverPos : String.Pos) : Bool := Id.run do
-  let some tailPos := i.tailPos?
-    | return false
-  return tailPos == hoverPos
-
 def Info.occursInside? (i : Info) (hoverPos : String.Pos) : Option String.Pos := do
   let headPos ← i.pos?
   let tailPos ← i.tailPos?
@@ -359,26 +354,28 @@ structure GoalsAtResult where
     where to show intermediate states by calling `withTacticInfoContext`) -/
 partial def InfoTree.goalsAt? (text : FileMap) (t : InfoTree) (hoverPos : String.Pos) : List GoalsAtResult :=
   let gs := t.collectNodesBottomUp fun ctx i cs gs => Id.run do
-    if let Info.ofTacticInfo ti := i then
-      if let (some pos, some tailPos) := (i.pos?, i.tailPos?) then
-        let trailSize := i.stx.getTrailingSize
-        -- show info at EOF even if strictly outside token + trail
-        let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
-        -- include at least one trailing character (see also `priority` below)
-        if pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + max 1 trailSize || atEOF) then
-          -- overwrite bottom-up results according to "innermost" heuristics documented above
-          if gs.isEmpty || hoverPos ≥ tailPos && gs.all (·.indented) then
-            return [{
-              ctxInfo := ctx
-              tacticInfo := ti
-              useAfter := hoverPos > pos && !cs.any (hasNestedTactic pos tailPos)
-              -- consider every position unindented after an empty `by` to support "hanging" `by` uses
-              indented := (text.toPosition pos).column > (text.toPosition hoverPos).column && !isEmptyBy ti.stx
-              -- use goals just before cursor as fall-back only
-              -- thus for `(by foo)`, placing the cursor after `foo` shows its state as long
-              -- as there is no state on `)`
-              priority := if hoverPos.byteIdx == tailPos.byteIdx + trailSize then 0 else 1
-            }]
+    let Info.ofTacticInfo ti := i
+      | return gs
+    let (some pos, some tailPos) := (i.pos?, i.tailPos?)
+      | return gs
+    let trailSize := i.stx.getTrailingSize
+    -- show info at EOF even if strictly outside token + trail
+    let atEOF := tailPos.byteIdx + trailSize == text.source.endPos.byteIdx
+    -- include at least one trailing character (see also `priority` below)
+    if pos ≤ hoverPos ∧ (hoverPos.byteIdx < tailPos.byteIdx + max 1 trailSize || atEOF) then
+      -- overwrite bottom-up results according to "innermost" heuristics documented above
+      if gs.isEmpty || hoverPos ≥ tailPos && gs.all (·.indented) then
+        return [{
+          ctxInfo := ctx
+          tacticInfo := ti
+          useAfter := hoverPos > pos && !cs.any (hasNestedTactic pos tailPos)
+          -- consider every position unindented after an empty `by` to support "hanging" `by` uses
+          indented := (text.toPosition pos).column > (text.toPosition hoverPos).column && !isEmptyBy ti.stx
+          -- use goals just before cursor as fall-back only
+          -- thus for `(by foo)`, placing the cursor after `foo` shows its state as long
+          -- as there is no state on `)`
+          priority := if hoverPos.byteIdx == tailPos.byteIdx + trailSize then 0 else 1
+        }]
     return gs
   let maxPrio? := gs.map (·.priority) |>.max?
   gs.filter (some ·.priority == maxPrio?)
diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean
index 9fbe1b5110c7..44dfbc88d333 100644
--- a/src/Lean/Server/Requests.lean
+++ b/src/Lean/Server/Requests.lean
@@ -210,6 +210,28 @@ partial def findInfoTreeAtPos
         some s.cmdState.infoState.trees[0]!
     | none => .pure none
 
+open Language in
+/--
+Finds the command syntax and info tree of the first snapshot task matching `isMatchingSnapshot` and
+containing `pos`, asynchronously. The info tree may be from a nested snapshot,
+such as a single tactic.
+
+See `SnapshotTree.findInfoTreeAtPos` for details on how the search is done.
+-/
+def findCmdDataAtPos
+    (doc : EditableDocument)
+    (isMatchingSnapshot : Lean.CommandParsedSnapshot → Bool)
+    (pos : String.Pos)
+    : Task (Option (Syntax × Elab.InfoTree)) :=
+  findCmdParsedSnap doc (isMatchingSnapshot ·) |>.bind (sync := true) fun
+    | some cmdParsed => toSnapshotTree cmdParsed |>.findInfoTreeAtPos pos |>.bind (sync := true) fun
+      | some infoTree => .pure <| some (cmdParsed.data.stx, infoTree)
+      | none          => cmdParsed.data.finishedSnap.task.map (sync := true) fun s =>
+        -- the parser returns exactly one command per snapshot, and the elaborator creates exactly one node per command
+        assert! s.cmdState.infoState.trees.size == 1
+        some (cmdParsed.data.stx, s.cmdState.infoState.trees[0]!)
+    | none => .pure none
+
 /--
 Finds the info tree of the first snapshot task containing `pos` (including trailing whitespace),
 asynchronously. The info tree may be from a nested snapshot, such as a single tactic.
diff --git a/tests/lean/interactive/completionTactics.lean b/tests/lean/interactive/completionTactics.lean
new file mode 100644
index 000000000000..110c4aa97410
--- /dev/null
+++ b/tests/lean/interactive/completionTactics.lean
@@ -0,0 +1,115 @@
+prelude
+import Init.Notation
+
+/-
+This test is a bit brittle because it checks that tactic completion works correctly for all
+tactic completions that we get in `prelude` + `import Init.Notation`.
+When changing the docstring of any of these tactics, this test will break.
+
+If you didn't touch the elaboration infrastructure or the language server, then you can safely
+assume that this test is still correct and unbreak it by overwriting
+`completionTactics.lean.expected.out` with `completionTactics.lean.produced.out` after running
+this test.
+-/
+
+/-- A docstring -/
+syntax (name := skip) "skip" : tactic
+
+/-- Another docstring -/
+syntax (name := exact) "exact " term : tactic
+
+example : True := by  -- No completions expected
+                  --^ textDocument/completion
+
+example : True := by   -- All tactic completions expected
+                   --^ textDocument/completion
+
+example : True := by ski  -- Tactic completions matching `ski` expected
+                      --^ textDocument/completion
+
+example : True := by skip  -- No completions expected
+                       --^ textDocument/completion
+
+example : True := by skip;  -- All tactic completions expected
+                        --^ textDocument/completion
+
+example : True := by skip;  -- All tactic completions expected
+                         --^ textDocument/completion
+
+example : True := by
+  skip
+  skip;  -- All tactic completions expected
+     --^ textDocument/completion
+
+example : True := by
+    -- All tactic completions expected
+--^ textDocument/completion
+
+example : True := by
+  skip
+    -- All tactic completions expected
+--^ textDocument/completion
+
+example : True := by
+    -- All tactic completions expected
+--^ textDocument/completion
+  skip
+
+example : True := by
+  exact by
+      -- All tactic completions expected
+  --^ textDocument/completion
+
+example : True := by
+  exact by
+      -- All tactic completions expected
+--^ textDocument/completion
+
+example : True := by
+  exact by
+    skip
+      -- All tactic completions expected
+  --^ textDocument/completion
+
+example : True := by
+  exact by
+    skip
+      -- All tactic completions expected
+--^ textDocument/completion
+
+example : True := by
+  exact
+      -- No completions expected
+  --^ textDocument/completion
+
+example : True := by
+  exact
+      -- All tactic completions expected
+--^ textDocument/completion
+
+example : True :=
+  let foo := by
+      -- All tactic completions expected
+  --^ textDocument/completion
+
+example : True :=
+  let foo := by
+      -- All tactic completions expected
+--^ textDocument/completion
+
+example : True :=
+  let foo := by
+    skip
+      -- All tactic completions expected
+  --^ textDocument/completion
+
+example : True :=
+  let foo := by
+    skip
+      -- No completions expected
+--^ textDocument/completion
+
+example : True := by {
+    -- All tactic completions expected
+--^ textDocument/completion
+}
diff --git a/tests/lean/interactive/completionTactics.lean.expected.out b/tests/lean/interactive/completionTactics.lean.expected.out
new file mode 100644
index 000000000000..8f0587690889
--- /dev/null
+++ b/tests/lean/interactive/completionTactics.lean.expected.out
@@ -0,0 +1,1712 @@
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 20, "character": 20}}
+{"items": [], "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 23, "character": 21}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 23, "character": 21}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 26, "character": 24}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 26, "character": 24}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 29, "character": 25}}
+{"items": [], "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 32, "character": 26}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 32, "character": 26}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 35, "character": 27}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 35, "character": 27}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 40, "character": 7}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 40, "character": 7}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 44, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 44, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 49, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 49, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 53, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 53, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 59, "character": 4}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 59, "character": 4}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 64, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 64, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 70, "character": 4}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 70, "character": 4}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 76, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 76, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 81, "character": 4}}
+{"items": [], "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 86, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 86, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 91, "character": 4}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 91, "character": 4}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 96, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 96, "character": 2}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 102, "character": 4}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 102, "character": 4}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 108, "character": 2}}
+{"items": [], "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionTactics.lean"},
+ "position": {"line": 112, "character": 2}}
+{"items":
+ [{"sortText": "0",
+   "label": "exact",
+   "kind": 14,
+   "documentation": {"value": "Another docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "1",
+   "label": "Lean.Parser.Tactic.decide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`decide` attempts to prove the main goal (with target type `p`) by synthesizing an instance of `Decidable p`\nand then reducing that instance to evaluate the truth value of `p`.\nIf it reduces to `isTrue h`, then `h` is a proof of `p` that closes the goal.\n\nLimitations:\n- The target is not allowed to contain local variables or metavariables.\n  If there are local variables, you can try first using the `revert` tactic with these local variables\n  to move them into the target, which may allow `decide` to succeed.\n- Because this uses kernel reduction to evaluate the term, `Decidable` instances defined\n  by well-founded recursion might not work, because evaluating them requires reducing proofs.\n  The kernel can also get stuck reducing `Decidable` instances with `Eq.rec` terms for rewriting propositions.\n  These can appear for instances defined using tactics (such as `rw` and `simp`).\n  To avoid this, use definitions such as `decidable_of_iff` instead.\n\n## Examples\n\nProving inequalities:\n```lean\nexample : 2 + 2 ≠ 5 := by decide\n```\n\nTrying to prove a false proposition:\n```lean\nexample : 1 ≠ 1 := by decide\n/-\ntactic 'decide' proved that the proposition\n  1 ≠ 1\nis false\n-/\n```\n\nTrying to prove a proposition whose `Decidable` instance fails to reduce\n```lean\nopaque unknownProp : Prop\n\nopen scoped Classical in\nexample : unknownProp := by decide\n/-\ntactic 'decide' failed for proposition\n  unknownProp\nsince its 'Decidable' instance reduced to\n  Classical.choice ⋯\nrather than to the 'isTrue' constructor.\n-/\n```\n\n## Properties and relations\n\nFor equality goals for types with decidable equality, usually `rfl` can be used in place of `decide`.\n```lean\nexample : 1 + 1 = 2 := by decide\nexample : 1 + 1 = 2 := by rfl\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "2",
+   "label": "Lean.Parser.Tactic.introMatch",
+   "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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "3",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "4",
+   "label": "Lean.Parser.Tactic.nativeDecide",
+   "kind": 14,
+   "documentation":
+   {"value":
+    "`native_decide` will attempt to prove a goal of type `p` by synthesizing an instance\nof `Decidable p` and then evaluating it to `isTrue ..`. Unlike `decide`, this\nuses `#eval` to evaluate the decidability instance.\n\nThis should be used with care because it adds the entire lean compiler to the trusted\npart, and the axiom `ofReduceBool` will show up in `#print axioms` for theorems using\nthis method or anything that transitively depends on them. Nevertheless, because it is\ncompiled, this can be significantly more efficient than using `decide`, and for very\nlarge computations this is one way to run external programs and trust the result.\n```\nexample : (List.range 1000).length = 1000 := by native_decide\n```\n",
+    "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "5",
+   "label": "Lean.Parser.Tactic.nestedTactic",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "6",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "7",
+   "label": "Lean.Parser.Tactic.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":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "8",
+   "label": "Lean.Parser.Tactic.unknown",
+   "kind": 14,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}},
+  {"sortText": "9",
+   "label": "skip",
+   "kind": 14,
+   "documentation": {"value": "A docstring ", "kind": "markdown"},
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionTactics.lean"},
+     "position": {"line": 112, "character": 2}}}}],
+ "isIncomplete": true}