diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index 64923174490b..ff91bfdb17a4 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -1435,8 +1435,9 @@ macro (name := declareSimpLikeTactic) doc?:(docComment)?
         | _ => `(config| (config := $updateCfg {}))
       let s := s.setKind $kind
       let s := s.setArg 0 (mkAtomFrom s[0] $tkn (canonical := true))
-      let r := s.setArg 1 (mkNullNode #[c])
-      return r)
+      let s := s.setArg 1 (mkNullNode #[c])
+      let s := s.mkSynthetic
+      return s)
 
 /-- `simp!` is shorthand for `simp` with `autoUnfold := true`.
 This will rewrite with all equation lemmas, which can be used to
diff --git a/tests/lean/interactive/issue5597.lean b/tests/lean/interactive/issue5597.lean
new file mode 100644
index 000000000000..4923f4a0e44f
--- /dev/null
+++ b/tests/lean/interactive/issue5597.lean
@@ -0,0 +1,3 @@
+example : True := by
+  simp!
+ --^ textDocument/hover
diff --git a/tests/lean/interactive/issue5597.lean.expected.out b/tests/lean/interactive/issue5597.lean.expected.out
new file mode 100644
index 000000000000..fcb826ad8cb3
--- /dev/null
+++ b/tests/lean/interactive/issue5597.lean.expected.out
@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file:///issue5597.lean"},
+ "position": {"line": 1, "character": 3}}
+{"range":
+ {"start": {"line": 1, "character": 2}, "end": {"line": 1, "character": 7}},
+ "contents":
+ {"value":
+  "`simp!` is shorthand for `simp` with `autoUnfold := true`.\nThis will rewrite with all equation lemmas, which can be used to\npartially evaluate many definitions. ",
+  "kind": "markdown"}}