diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index d3324bac9c..cde43a624c 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -666,6 +666,50 @@ private def tacticCompletion (params : CompletionParams) (ctx : ContextInfo) : I
       }, 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)
+    (infoTree : InfoTree)
+    : Option (ContextInfo × Info) :=
+  infoTree.visitM (m := Id) (postNode := choose) |>.join
+where
+  choose
+      (ctx : ContextInfo)
+      (info : Info)
+      (_ : PersistentArray InfoTree)
+      (childValues : List (Option (Option (ContextInfo × Info))))
+      : Option (ContextInfo × Info) :=
+    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)
+    else
+      bestChildValue
+
+  isBetter (a b : Option (ContextInfo × Info)) : 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
+
 private def findCompletionInfoAt?
     (fileMap  : FileMap)
     (hoverPos : String.Pos)
@@ -675,9 +719,32 @@ private def findCompletionInfoAt?
   match infoTree.foldInfo (init := none) (choose hoverLine) with
   | some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
     some (hoverInfo, ctx, info)
-  | _ =>
-    -- TODO try to extract id from `fileMap` and some `ContextInfo` from `InfoTree`
-    none
+  | _ => 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)
 where
   choose
       (hoverLine : Nat)
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 70c8172988..361c37d39c 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -141,10 +141,12 @@ def Info.stx : Info → Syntax
   | ofOmissionInfo i       => i.stx
 
 def Info.lctx : Info → LocalContext
-  | Info.ofTermInfo i     => i.lctx
-  | Info.ofFieldInfo i    => i.lctx
-  | Info.ofOmissionInfo i => i.lctx
-  | _                     => LocalContext.empty
+  | .ofTermInfo i           => i.lctx
+  | .ofFieldInfo i          => i.lctx
+  | .ofOmissionInfo i       => i.lctx
+  | .ofMacroExpansionInfo i => i.lctx
+  | .ofCompletionInfo i     => i.lctx
+  | _                       => LocalContext.empty
 
 def Info.pos? (i : Info) : Option String.Pos :=
   i.stx.getPos? (canonicalOnly := true)
diff --git a/tests/lean/interactive/completionFallback.lean b/tests/lean/interactive/completionFallback.lean
new file mode 100644
index 0000000000..5297577e11
--- /dev/null
+++ b/tests/lean/interactive/completionFallback.lean
@@ -0,0 +1,31 @@
+-- When the elaborator doesn't provide `CompletionInfo`, try to provide identifier completions.
+-- As of when this test case was written, the elaborator did not provide `CompletionInfo` in these cases.
+
+-- https://github.com/leanprover/lean4/issues/5172
+
+inductive Direction where
+  | up
+  | right
+  | down
+  | left
+deriving Repr
+
+def angle (d: Direction) :=
+  match d with
+  | Direction. => 90
+            --^ textDocument/completion
+  | Direction.right => 0
+  | Direction.down => 270
+  | Direction.left => 180
+
+-- Ensure that test is stable when changes to the `And` namespace are made.
+structure CustomAnd (a b : Prop) : Prop where
+  ha : a
+  hb : b
+
+example : p ∨ (q ∧ r) → CustomAnd (p ∨ q) (p ∨ r) := by
+  intro h
+  cases h with
+  | inl hp => apply CustomAnd. (Or.intro_left q hp) (Or.intro_left r hp)
+                            --^ textDocument/completion
+  | inr hqr => apply CustomAnd.mk (Or.intro_right p hqr.left) (Or.intro_right p hqr.right)
diff --git a/tests/lean/interactive/completionFallback.lean.expected.out b/tests/lean/interactive/completionFallback.lean.expected.out
new file mode 100644
index 0000000000..7cd2e288a0
--- /dev/null
+++ b/tests/lean/interactive/completionFallback.lean.expected.out
@@ -0,0 +1,80 @@
+{"textDocument": {"uri": "file:///completionFallback.lean"},
+ "position": {"line": 14, "character": 14}}
+{"items":
+ [{"sortText": "0",
+   "label": "down",
+   "kind": 4,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 14, "character": 14}},
+    "id": {"const": {"declName": "Direction.down"}}}},
+  {"sortText": "1",
+   "label": "left",
+   "kind": 4,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 14, "character": 14}},
+    "id": {"const": {"declName": "Direction.left"}}}},
+  {"sortText": "2",
+   "label": "noConfusionType",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 14, "character": 14}},
+    "id": {"const": {"declName": "Direction.noConfusionType"}}}},
+  {"sortText": "3",
+   "label": "right",
+   "kind": 4,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 14, "character": 14}},
+    "id": {"const": {"declName": "Direction.right"}}}},
+  {"sortText": "4",
+   "label": "toCtorIdx",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 14, "character": 14}},
+    "id": {"const": {"declName": "Direction.toCtorIdx"}}}},
+  {"sortText": "5",
+   "label": "up",
+   "kind": 4,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 14, "character": 14}},
+    "id": {"const": {"declName": "Direction.up"}}}}],
+ "isIncomplete": true}
+{"textDocument": {"uri": "file:///completionFallback.lean"},
+ "position": {"line": 28, "character": 30}}
+{"items":
+ [{"sortText": "0",
+   "label": "ha",
+   "kind": 5,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 28, "character": 30}},
+    "id": {"const": {"declName": "CustomAnd.ha"}}}},
+  {"sortText": "1",
+   "label": "hb",
+   "kind": 5,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 28, "character": 30}},
+    "id": {"const": {"declName": "CustomAnd.hb"}}}},
+  {"sortText": "2",
+   "label": "mk",
+   "kind": 4,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionFallback.lean"},
+     "position": {"line": 28, "character": 30}},
+    "id": {"const": {"declName": "CustomAnd.mk"}}}}],
+ "isIncomplete": true}
diff --git a/tests/lean/interactive/fieldCompletion.lean b/tests/lean/interactive/fieldCompletion.lean
deleted file mode 100644
index 2d9ad2627c..0000000000
--- a/tests/lean/interactive/fieldCompletion.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Lean
-
-open Lean Elab
-
-def f (s : DefView) : DefView := {
-  m
- --^ textDocument/completion
-}
diff --git a/tests/lean/interactive/fieldCompletion.lean.expected.out b/tests/lean/interactive/fieldCompletion.lean.expected.out
deleted file mode 100644
index 527d9d7e87..0000000000
--- a/tests/lean/interactive/fieldCompletion.lean.expected.out
+++ /dev/null
@@ -1,3 +0,0 @@
-{"textDocument": {"uri": "file:///fieldCompletion.lean"},
- "position": {"line": 5, "character": 3}}
-{"items": [], "isIncomplete": true}