diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean
index 155828f34d..72d0f44f7c 100644
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Main.lean
+++ b/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 <|
diff --git a/tests/lean/run/partial_fixpoint.lean b/tests/lean/run/partial_fixpoint.lean
index 765aed9202..16d1688aef 100644
--- a/tests/lean/run/partial_fixpoint.lean
+++ b/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