refactor: rename new option to debug.rawDecreasingByGoal (#5066)

as suggested by @semorrison in 

https://leanprover.zulipchat.com/#narrow/stream/116290-rss/topic/cleanDecreasingBy/near/462659021


Follow-up to #5016.

Author: nomeata

src/Lean/Elab/PreDefinition/WF/Basic.lean

@@ -9,17 +9,17 @@ import Lean.Elab.Tactic.Basic
 
 namespace Lean.Elab.WF
 
-register_builtin_option cleanDecreasingByGoal : Bool := {
-  defValue := true
-  descr    := "Cleans up internal implementation details in the proof goals presented by \
-              `decreasing_by`, using the `clean_wf` tactic. Can be disabled for debugging \
-              purposes. Please report an issue if you have to disable this option."
+register_builtin_option debug.rawDecreasingByGoal : Bool := {
+  defValue := false
+  descr    := "Shows the raw `decreasing_by` goal including internal implementation detail \
+               intead of cleaning it up with the `clean_wf` tactic. Can be enabled for debugging \
+               purposes. Please report an issue if you have to use this option for other reasons."
 }
 
 open Lean Elab Tactic
 
 def applyCleanWfTactic : TacticM Unit := do
-  if cleanDecreasingByGoal.get (← getOptions) then
+  unless debug.rawDecreasingByGoal.get (← getOptions) do
     Tactic.evalTactic (← `(tactic| all_goals clean_wf))
 
 end Lean.Elab.WF

tests/lean/run/4928.lean

@@ -58,7 +58,7 @@ y : Nat
     (PSum.inr ⟨x.tail, y⟩) (PSum.inl ⟨x, y⟩)
 -/
 #guard_msgs in
-set_option cleanDecreasingByGoal false in
+set_option debug.rawDecreasingByGoal true in
 mutual
 def g1 (x : List Nat) (y : Nat) : Nat := g2 x.tail y
 termination_by x.length