diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean
index 8fb4cffc03..97ff51ce9d 100644
--- a/src/Lean/Server/Completion/CompletionCollectors.lean
+++ b/src/Lean/Server/Completion/CompletionCollectors.lean
@@ -65,32 +65,12 @@ section Infrastructure
       (score         : Float)
       : M Unit := do
     let env ← getEnv
-    let (docStringPrefix?, tags?) := Id.run do
+    let tags? := do
       let .const declName := id
-        | (none, none)
-      let some param := Linter.deprecatedAttr.getParam? env declName
-        | (none, none)
-      let docstringPrefix :=
-        if let some text := param.text? then
-          text
-        else if let some newName := param.newName? then
-          s!"`{declName}` has been deprecated, use `{newName}` instead."
-        else
-          s!"`{declName}` has been deprecated."
-      (some docstringPrefix, some #[CompletionItemTag.deprecated])
-    let docString? ← do
-      let .const declName := id
-        | pure none
-      findDocString? env declName
-    let doc? := do
-      let docValue ←
-        match docStringPrefix?, docString? with
-        | none,                 none           => none
-        | some docStringPrefix, none           => docStringPrefix
-        | none,                 docString      => docString
-        | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}"
-      pure { value := docValue , kind := MarkupKind.markdown : MarkupContent }
-    let item := { label := label.toString, kind? := kind, documentation? := doc?, tags?}
+        | none
+      guard <| Linter.isDeprecated env declName
+      some #[CompletionItemTag.deprecated]
+    let item := { label := label.toString, kind? := kind, tags? }
     addItem item score id
 
   private def getCompletionKindForDecl (constInfo : ConstantInfo) : M CompletionItemKind := do
diff --git a/src/Lean/Server/Completion/CompletionResolution.lean b/src/Lean/Server/Completion/CompletionResolution.lean
index 48e4302c3d..c071840192 100644
--- a/src/Lean/Server/Completion/CompletionResolution.lean
+++ b/src/Lean/Server/Completion/CompletionResolution.lean
@@ -62,6 +62,34 @@ def CompletionItem.resolve
         return toString (← Meta.ppExpr typeWithoutImplicits)
     item := { item with detail? := detail? }
 
+  if item.documentation?.isNone then
+    let docStringPrefix? := Id.run do
+      let .const declName := id
+        | none
+      let some param := Linter.deprecatedAttr.getParam? env declName
+        | none
+      let docstringPrefix :=
+        if let some text := param.text? then
+          text
+        else if let some newName := param.newName? then
+          s!"`{declName}` has been deprecated, use `{newName}` instead."
+        else
+          s!"`{declName}` has been deprecated."
+      some docstringPrefix
+    let docString? ← do
+      let .const declName := id
+        | pure none
+      findDocString? env declName
+    let doc? := do
+      let docValue ←
+        match docStringPrefix?, docString? with
+        | none,                 none           => none
+        | some docStringPrefix, none           => docStringPrefix
+        | none,                 docString      => docString
+        | some docStringPrefix, some docString => s!"{docStringPrefix}\n\n{docString}"
+      pure { value := docValue , kind := MarkupKind.markdown : MarkupContent }
+    item := { item with documentation? := doc? }
+
   return item
 
 end Lean.Lsp
diff --git a/tests/lean/interactive/1265.lean.expected.out b/tests/lean/interactive/1265.lean.expected.out
index 0f91b29507..92cc3b8184 100644
--- a/tests/lean/interactive/1265.lean.expected.out
+++ b/tests/lean/interactive/1265.lean.expected.out
@@ -85,8 +85,6 @@
   {"sortText": "9",
    "label": "raw",
    "kind": 5,
-   "documentation":
-   {"value": "The underlying `Syntax` value. ", "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///1265.lean"},
@@ -181,8 +179,6 @@
   {"sortText": "9",
    "label": "raw",
    "kind": 5,
-   "documentation":
-   {"value": "The underlying `Syntax` value. ", "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///1265.lean"},
diff --git a/tests/lean/interactive/completionDeprecation.lean.expected.out b/tests/lean/interactive/completionDeprecation.lean.expected.out
index 1550a8f6ea..e32f3a19ff 100644
--- a/tests/lean/interactive/completionDeprecation.lean.expected.out
+++ b/tests/lean/interactive/completionDeprecation.lean.expected.out
@@ -13,7 +13,6 @@
   {"sortText": "1",
    "label": "foo2",
    "kind": 3,
-   "documentation": {"value": "A docstring. ", "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
@@ -24,8 +23,6 @@
    "sortText": "2",
    "label": "foo3",
    "kind": 3,
-   "documentation":
-   {"value": "`SomeStructure.foo3` has been deprecated.", "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
@@ -36,9 +33,6 @@
    "sortText": "3",
    "label": "foo4",
    "kind": 3,
-   "documentation":
-   {"value": "`SomeStructure.foo4` has been deprecated.\n\nA docstring. ",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
@@ -49,10 +43,6 @@
    "sortText": "4",
    "label": "foo5",
    "kind": 3,
-   "documentation":
-   {"value":
-    "`SomeStructure.foo5` has been deprecated, use `SomeStructure.foo1` instead.",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
@@ -63,10 +53,6 @@
    "sortText": "5",
    "label": "foo6",
    "kind": 3,
-   "documentation":
-   {"value":
-    "`SomeStructure.foo6` has been deprecated, use `SomeStructure.foo1` instead.\n\nA docstring. ",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
@@ -77,10 +63,6 @@
    "sortText": "6",
    "label": "foo7",
    "kind": 3,
-   "documentation":
-   {"value":
-    "`SomeStructure.foo7` has been deprecated; please use `SomeStructure.foo1` instead.",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
@@ -91,10 +73,6 @@
    "sortText": "7",
    "label": "foo8",
    "kind": 3,
-   "documentation":
-   {"value":
-    "`SomeStructure.foo8` has been deprecated; please use `SomeStructure.foo1` instead.\n\nA docstring. ",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionDeprecation.lean"},
diff --git a/tests/lean/interactive/completionDocString.lean b/tests/lean/interactive/completionDocString.lean
deleted file mode 100644
index 4711f7e99f..0000000000
--- a/tests/lean/interactive/completionDocString.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-#eval Array.insertIdx
-                   --^ textDocument/completion
diff --git a/tests/lean/interactive/completionDocString.lean.expected.out b/tests/lean/interactive/completionDocString.lean.expected.out
deleted file mode 100644
index 5e16bdbe37..0000000000
--- a/tests/lean/interactive/completionDocString.lean.expected.out
+++ /dev/null
@@ -1,41 +0,0 @@
-{"textDocument": {"uri": "file:///completionDocString.lean"},
- "position": {"line": 0, "character": 21}}
-{"items":
- [{"sortText": "0",
-   "label": "insertIdx",
-   "kind": 3,
-   "documentation":
-   {"value": "Insert element `a` at position `i`. ", "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 21}},
-    "id": {"const": {"declName": "Array.insertIdx"}},
-    "cPos": 0}},
-  {"sortText": "1",
-   "label": "insertIdxIfInBounds",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Insert element `a` at position `i`, or do nothing if `as.size < i`. ",
-    "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 21}},
-    "id": {"const": {"declName": "Array.insertIdxIfInBounds"}},
-    "cPos": 0}},
-  {"sortText": "2",
-   "label": "insertIdx!",
-   "kind": 3,
-   "documentation":
-   {"value":
-    "Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. ",
-    "kind": "markdown"},
-   "data":
-   {"params":
-    {"textDocument": {"uri": "file:///completionDocString.lean"},
-     "position": {"line": 0, "character": 21}},
-    "id": {"const": {"declName": "Array.insertIdx!"}},
-    "cPos": 0}}],
- "isIncomplete": true}
diff --git a/tests/lean/interactive/completionPrv.lean.expected.out b/tests/lean/interactive/completionPrv.lean.expected.out
index 319c5da1fd..a81d2fa8b2 100644
--- a/tests/lean/interactive/completionPrv.lean.expected.out
+++ b/tests/lean/interactive/completionPrv.lean.expected.out
@@ -89,9 +89,6 @@
   {"sortText": "8",
    "label": "BitVec.ofBoolListBE",
    "kind": 3,
-   "documentation":
-   {"value": "Converts a list of `Bool`s to a big-endian `BitVec`. ",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///completionPrv.lean"},
diff --git a/tests/lean/interactive/travellingCompletions.lean.expected.out b/tests/lean/interactive/travellingCompletions.lean.expected.out
index b04e4b81cd..412c2bf6a1 100644
--- a/tests/lean/interactive/travellingCompletions.lean.expected.out
+++ b/tests/lean/interactive/travellingCompletions.lean.expected.out
@@ -65,10 +65,6 @@
  [{"sortText": "0",
    "label": "intro",
    "kind": 4,
-   "documentation":
-   {"value":
-    "`True` is true, and `True.intro` (or more commonly, `trivial`)\nis the proof. ",
-    "kind": "markdown"},
    "data":
    {"params":
     {"textDocument": {"uri": "file:///travellingCompletions.lean"},