fix: suggest correct trace option name in partial_fixpoint error message (#6774)

This PR fixes a `partial_fixpoint` error message to suggest the option
`trace.Elab.Tactic.monotonicity` rather than the nonexistent
`trace.Elab.Tactic.partial_monotonicity`.

src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean

@@ -112,7 +112,7 @@ def partialFixpoint (preDefs : Array PreDefinition) : TermElabM Unit := do
         let extraMsg := if monoThms.isEmpty then m!"" else
           m!"Tried to apply {.andList (monoThms.toList.map (m!"'{.ofConstName ·}'"))}, but failed.\n\
              Possible cause: A missing `{.ofConstName ``MonoBind}` instance.\n\
-             Use `set_option trace.Elab.Tactic.partial_monotonicity true` to debug."
+             Use `set_option trace.Elab.Tactic.monotonicity true` to debug."
         if let some recApp := t.find? hasRecAppSyntax then
           let some syn := getRecAppSyntax? recApp | panic! "getRecAppSyntax? failed"
           withRef syn <|

tests/lean/run/partial_fixpoint.lean

@@ -283,7 +283,7 @@ error: Could not prove 'WrongMonad.ack' to be monotone in its recursive calls:
       ack x✝ __do_lift
   Tried to apply 'Lean.Order.monotone_bind', but failed.
   Possible cause: A missing `Lean.Order.MonoBind` instance.
-  Use `set_option trace.Elab.Tactic.partial_monotonicity true` to debug.
+  Use `set_option trace.Elab.Tactic.monotonicity true` to debug.
 -/
 #guard_msgs in
 def WrongMonad.ack : (n m : Nat) → Id Nat
@@ -369,7 +369,7 @@ error: Could not prove 'Tree.rev'''' to be monotone in its recursive calls:
           { cs := ts.toList })
   Tried to apply 'Lean.Order.Array.monotone_mapFinIdxM', but failed.
   Possible cause: A missing `Lean.Order.MonoBind` instance.
-  Use `set_option trace.Elab.Tactic.partial_monotonicity true` to debug.
+  Use `set_option trace.Elab.Tactic.monotonicity true` to debug.
 -/
 #guard_msgs in
 def Tree.rev''' (ts : Array Tree) : Id (Array Tree) := do