chore(Tactic/FunProp): reword failure hint (#37339)

Reword ``Maybe you forgot marking `{decl}` with `@[fun_prop]`.`` to ``Consider marking `{decl}` with `@[fun_prop]`.``.

Author: SnirBroshi

Mathlib/Tactic/FunProp/Elab.lean

@@ -79,7 +79,7 @@ def funPropTac : Tactic
         unless (← getFunProp? type).isSome do
           let hint :=
             if let some n := type.getAppFn.constName?
-            then s!" Maybe you forgot marking `{n}` with `@[fun_prop]`."
+            then s!" Consider marking `{n}` with `@[fun_prop]`."
             else ""
           throwError "`{← ppExpr type}` is not a `fun_prop` goal!{hint}"
 

MathlibTest/fun_prop_dev.lean

@@ -397,6 +397,11 @@ end MultipleLambdaTheorems
 #guard_msgs in
 #check_failure ((by fun_prop) : ?m)
 
+/-- error: `Injective Nat.succ` is not a `fun_prop` goal!
+Consider marking `Function.Injective` with `@[fun_prop]`. -/
+#guard_msgs in
+example : Nat.succ.Injective := by fun_prop
+
 -- todo: warning should not have mvar id in it
 -- /-- warning: `?m.71721` is not a `fun_prop` goal! -/
 -- #guard_msgs in