fix: declareSimpLikeTactic macro to use mkSynthetic (#5838)

this fixes #5597

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

tests/lean/interactive/issue5597.lean

@@ -0,0 +1,3 @@
+example : True := by
+  simp!
+ --^ textDocument/hover

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"}}