diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index a91d398537..11b32b9b36 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -109,7 +109,17 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
           let major := e.getArg! projInfo.numParams
           unless (← isConstructorApp major) do
             return none
-          reduceProjCont? (← unfoldDefinitionAny? e)
+          if backward.whnf.reducibleClassField.get (← getOptions) then
+            /-
+            When `backward.whnf.reducibleClassField` is `true`, `unfoldDefault` (in WHNF.lean)
+            already reduces the `.proj` node during `unfoldDefinitionAny?`, so `reduceProjCont?`
+            would discard the fully-reduced result because it expects a `.proj` head.
+            We return the unfolded result directly; the dsimp traversal will revisit it
+            (via `.visit`) and handle any remaining `.proj` nodes naturally.
+            -/
+            unfoldDefinitionAny? e
+          else
+            reduceProjCont? (← unfoldDefinitionAny? e)
       else
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
diff --git a/tests/lean/run/simp_reducibleClassField.lean b/tests/lean/run/simp_reducibleClassField.lean
new file mode 100644
index 0000000000..047e698f22
--- /dev/null
+++ b/tests/lean/run/simp_reducibleClassField.lean
@@ -0,0 +1,9 @@
+set_option backward.whnf.reducibleClassField true in
+example [Ord α] {a b : α} :
+    (letI : Ord α := ⟨fun a b => compare b a⟩; compare a b) = compare b a := by
+  simp only
+
+set_option backward.whnf.reducibleClassField true in
+example [Ord α] {a b : α} :
+    (letI : Ord α := ⟨fun a b => compare b a⟩; compare a b) = compare b a := by
+  simp