diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean
index 8a3c6e7c36..2587a0f442 100644
--- a/src/Lean/Meta/Tactic/Unfold.lean
+++ b/src/Lean/Meta/Tactic/Unfold.lean
@@ -25,7 +25,9 @@ where
   pre (unfoldThm : Name) (e : Expr) : SimpM Simp.Step := do
     match (← withReducible <| Simp.tryTheorem? e { proof := mkConst unfoldThm, name? := some unfoldThm, rfl := (← isRflTheorem unfoldThm) } (fun _ => return none)) with
     | none   => pure ()
-    | some r => return Simp.Step.done r
+    | some r => match (← reduceMatcher? r.expr) with
+      | .reduced e' => return Simp.Step.done { r with expr := e' }
+      | _ => return Simp.Step.done r
     return Simp.Step.visit { expr := e }
 
 def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := withMVarContext mvarId do
diff --git a/tests/lean/unfoldReduceMatch.lean b/tests/lean/unfoldReduceMatch.lean
new file mode 100644
index 0000000000..2af4a5c273
--- /dev/null
+++ b/tests/lean/unfoldReduceMatch.lean
@@ -0,0 +1,5 @@
+open Nat
+example : Nat.add zero (succ n) = succ n := by
+  unfold Nat.add
+  trace_state
+  sorry
diff --git a/tests/lean/unfoldReduceMatch.lean.expected.out b/tests/lean/unfoldReduceMatch.lean.expected.out
new file mode 100644
index 0000000000..924b7c25e4
--- /dev/null
+++ b/tests/lean/unfoldReduceMatch.lean.expected.out
@@ -0,0 +1,3 @@
+unfoldReduceMatch.lean:5:2-5:7: warning: declaration uses 'sorry'
+n : Nat
+⊢ Nat.succ (Nat.add Nat.zero n) = Nat.succ n