feat: unfold tactic tries to reduce match after unfolding

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

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

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