Tweak messages, be more opinionated about string replacement, and fix tests

Author: robsimmons

src/Init/Data/String/Search.lean

@@ -332,7 +332,7 @@ def contains (s : String) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
 def Internal.containsImpl (s : String) (c : Char) : Bool :=
   String.contains s c
 
-@[inline, inherit_doc contains, suggest_for String.some]
+@[inline, inherit_doc contains]
 def any (s : String) (pat : ρ) [ToForwardSearcher pat σ] : Bool :=
   s.contains pat
 

src/Lean/Elab/App.lean

@@ -1434,7 +1434,7 @@ where
           (suggestions.map fun suggestion => {
             preInfo? := .some ".",
             suggestion := suggestion.getString!,
-            toCodeActionTitle? := .some (s!"Change to {e}.{·}"),
+            toCodeActionTitle? := .some (s!"Change to .{·}"),
             diffGranularity := .all,
           })
       else

tests/lean/run/idSuggestEvery.lean

@@ -19,7 +19,7 @@ of type
 error: Unknown constant `Subarray.every`
 
 Hint: Perhaps you meant `Subarray.all` in place of `Subarray.every`:
-  S̵u̵b̵a̵r̵r̵a̵y̵.̵e̵v̵e̵r̵y̵S̲u̲b̲a̲r̲r̲a̲y̲.̲a̲l̲l̲
+  [apply] `Subarray.all`
 -/
 #guard_msgs in example := (@Subarray.every Nat (fun _ => true) ·)
 #guard_msgs in example := (@Subarray.all Nat (fun _ => true) ·)
@@ -28,7 +28,7 @@ Hint: Perhaps you meant `Subarray.all` in place of `Subarray.every`:
 error: Unknown constant `Subarray.some`
 
 Hint: Perhaps you meant `Subarray.any` in place of `Subarray.some`:
-  S̵u̵b̵a̵r̵r̵a̵y̵.̵s̵o̵m̵e̵S̲u̲b̲a̲r̲r̲a̲y̲.̲a̲n̲y̲
+  [apply] `Subarray.any`
 -/
 #guard_msgs in example := (@Subarray.some Nat (fun _ => true) ·)
 #guard_msgs in example := (@Subarray.any Nat (fun _ => true) ·)
@@ -48,12 +48,11 @@ error: Invalid field `some`: The environment does not contain `String.some`, so
   x
 of type `String`
 
-Hint: Perhaps you meant one of these in place of `String.some`:
-  [apply] `String.contains`
-  [apply] `String.any`
+Hint: Perhaps you meant `String.contains` in place of `String.some`:
+  .s̵o̵m̵e̵c̲o̲n̲t̲a̲i̲n̲s̲
 -/
 #guard_msgs in example (x : String) := x.some fun _ => true
-#guard_msgs in example (x : String) := x.all fun _ => true
+#guard_msgs in example (x : String) := x.contains fun _ => true
 
 
 /--

tests/lean/run/idSuggestStandalone.lean

@@ -43,7 +43,7 @@ Hint: Perhaps you meant `String.foo` in place of `String.test0`:
 error: Unknown constant `String.test0`
 
 Hint: Perhaps you meant `String.foo` in place of `String.test0`:
-  S̵t̵r̵i̵n̵g̵.̵t̵e̵s̵t̵0̵S̲t̲r̲i̲n̲g̲.̲f̲o̲o̲
+  [apply] `String.foo`
 ---
 info: fun x1 x2 x3 => sorry : (x1 : ?m.1) → (x2 : ?m.5 x1) → (x3 : ?m.6 x1 x2) → ?m.7 x1 x2 x3
 -/