chore: update stage0

stage0/src/Lean/Elab/Tactic/Simp.lean

@@ -141,7 +141,10 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool)
             thms := thms.eraseCore arg[1].getId
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            thms ← thms.erase declName
+            if ctx.config.autoUnfold then
+              thms := thms.eraseCore declName
+            else
+              thms ← thms.erase declName
         else if arg.getKind == ``Lean.Parser.Tactic.simpLemma then
           let post :=
             if arg[0].isNone then

stage0/src/Lean/Meta/Tactic/Simp/Main.lean

@@ -94,6 +94,25 @@ private def reduceFVar (cfg : Config) (e : Expr) : MetaM Expr := do
   else
     return e
 
+/--
+  Return true if `declName` is the name of a definition of the form
+  ```
+  def declName ... :=
+    match ... with
+    | ...
+  ```
+-/
+private partial def isMatchDef (declName : Name) : CoreM Bool := do
+  let .defnInfo info ← getConstInfo declName | return false
+  return go (← getEnv) info.value
+where
+  go (env : Environment) (e : Expr) : Bool :=
+    if e.isLambda then
+      go env e.bindingBody!
+    else
+      let f := e.getAppFn
+      f.isConst && isMatcherCore env f.constName!
+
 private def unfold? (e : Expr) : SimpM (Option Expr) := do
   let f := e.getAppFn
   if !f.isConst then
@@ -101,7 +120,19 @@ private def unfold? (e : Expr) : SimpM (Option Expr) := do
   let fName := f.constName!
   if (← isProjectionFn fName) then
     return none -- should be reduced by `reduceProjFn?`
-  if (← read).isDeclToUnfold e.getAppFn.constName! then
+  let ctx ← read
+  if ctx.config.autoUnfold then
+    if ctx.simpTheorems.isErased fName then
+      return none
+    else if hasSmartUnfoldingDecl (← getEnv) fName then
+      withDefault <| unfoldDefinition? e
+    else if (← isMatchDef fName) then
+      let some value ← withDefault <| unfoldDefinition? e | return none
+      let .reduced value ← reduceMatcher? value | return none
+      return some value
+    else
+      return none
+  else if ctx.isDeclToUnfold fName then
     withDefault <| unfoldDefinition? e
   else
     return none