diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index b6a8739809..883ba7da88 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -199,7 +199,7 @@ def evalTacticCDot : Tactic := fun stx => do
   -- but the token antiquotation does not copy trailing whitespace, leading to
   -- differences in the goal display (#2153)
   let initInfo ← mkInitialTacticInfo stx[0]
-  withRef stx[0] <| closeUsingOrAdmit do
+  withCaseRef stx[0] stx[1] <| closeUsingOrAdmit do
     -- save state before/after entering focus on `·`
     withInfoContext (pure ()) initInfo
     Term.withNarrowedArgTacticReuse (argIdx := 1) evalTactic stx
diff --git a/tests/lean/interactive/issue4527.lean b/tests/lean/interactive/issue4527.lean
new file mode 100644
index 0000000000..407eb42452
--- /dev/null
+++ b/tests/lean/interactive/issue4527.lean
@@ -0,0 +1,5 @@
+example : True :=  by
+  . skip
+    --^ collectDiagnostics
+    skip
+    -- foo
diff --git a/tests/lean/interactive/issue4527.lean.expected.out b/tests/lean/interactive/issue4527.lean.expected.out
new file mode 100644
index 0000000000..0a542d8842
--- /dev/null
+++ b/tests/lean/interactive/issue4527.lean.expected.out
@@ -0,0 +1,10 @@
+{"version": 1,
+ "uri": "file:///issue4527.lean",
+ "diagnostics":
+ [{"source": "Lean 4",
+   "severity": 1,
+   "range":
+   {"start": {"line": 1, "character": 2}, "end": {"line": 2, "character": 0}},
+   "message": "unsolved goals\n⊢ True",
+   "fullRange":
+   {"start": {"line": 1, "character": 2}, "end": {"line": 3, "character": 8}}}]}
diff --git a/tests/lean/refineFiltersOldMVars.lean.expected.out b/tests/lean/refineFiltersOldMVars.lean.expected.out
index f0912d5d24..2bdca00e0a 100644
--- a/tests/lean/refineFiltersOldMVars.lean.expected.out
+++ b/tests/lean/refineFiltersOldMVars.lean.expected.out
@@ -9,12 +9,12 @@ h : Type
 case a
 ⊢ Type
 refineFiltersOldMVars.lean:66:4-66:11: error: no goals to be solved
-refineFiltersOldMVars.lean:101:2-101:3: error: unsolved goals
+refineFiltersOldMVars.lean:101:2-101:13: error: unsolved goals
 case d
 ⊢ Bool
-refineFiltersOldMVars.lean:102:2-102:3: error: unsolved goals
+refineFiltersOldMVars.lean:102:2-102:13: error: unsolved goals
 case e
 ⊢ Nat
-refineFiltersOldMVars.lean:109:2-109:3: error: unsolved goals
+refineFiltersOldMVars.lean:109:2-109:13: error: unsolved goals
 case e
 ⊢ Bool
diff --git a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
index 7f6b5a7382..ad43b70d2b 100644
--- a/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
+++ b/tests/lean/tacUnsolvedGoalsErrors.lean.expected.out
@@ -32,13 +32,13 @@ p q r : Prop
 h2 : p → q
 h✝ : q
 ⊢ q
-tacUnsolvedGoalsErrors.lean:26:2-26:3: error: unsolved goals
+tacUnsolvedGoalsErrors.lean:26:2-27:8: error: unsolved goals
 case inl
 p q r : Prop
 h2 : p → q
 h✝ : p
 ⊢ q
-tacUnsolvedGoalsErrors.lean:28:2-28:3: error: unsolved goals
+tacUnsolvedGoalsErrors.lean:28:2-29:8: error: unsolved goals
 case inr
 p q r : Prop
 h2 : p → q