fix: simp at local declaration should not create an auxiliary declaration when result is definitionally equal

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

@@ -734,22 +734,34 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Di
   withMVarContext mvarId do
     checkNotAssigned mvarId `simp
     let mut mvarId := mvarId
-    let mut toAssert : Array Hypothesis := #[]
+    let mut toAssert := #[]
+    let mut replaced := #[]
     for fvarId in fvarIdsToSimp do
       let localDecl ← getLocalDecl fvarId
       let type ← instantiateMVars localDecl.type
       let ctx ← match fvarIdToLemmaId.find? localDecl.fvarId with
         | none => pure ctx
         | some thmId => pure { ctx with simpTheorems := ctx.simpTheorems.eraseTheorem thmId }
-      match (← simpStep mvarId (mkFVar fvarId) type ctx discharge?) with
-      | none => return none
-      | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
-    if simplifyTarget then
+      let r ← simp type ctx discharge?
+      match r.proof? with
+      | some proof => match (← applySimpResultToProp mvarId (mkFVar fvarId) type r) with
+        | none => return none
+        | some (value, type) => toAssert := toAssert.push { userName := localDecl.userName, type := type, value := value }
+      | none =>
+        if r.expr.isConstOf ``False then
+          assignExprMVar mvarId (← mkFalseElim (← getMVarType mvarId) (mkFVar fvarId))
+          return none
+        -- TODO: if there are no forwards dependencies we may consider using the same approach we used when `r.proof?` is a `some ...`
+        -- Reason: it introduces a `mkExpectedTypeHint`
+        mvarId ← replaceLocalDeclDefEq mvarId fvarId r.expr
+        replaced := replaced.push fvarId
+     if simplifyTarget then
       match (← simpTarget mvarId ctx discharge?) with
       | none => return none
       | some mvarIdNew => mvarId := mvarIdNew
     let (fvarIdsNew, mvarIdNew) ← assertHypotheses mvarId toAssert
-    let mvarIdNew ← tryClearMany mvarIdNew fvarIdsToSimp
+    let toClear := fvarIdsToSimp.filter fun fvarId => !replaced.contains fvarId
+    let mvarIdNew ← tryClearMany mvarIdNew toClear
     return (fvarIdsNew, mvarIdNew)
 
 def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none) : MetaM TacticResultCNM := withMVarContext mvarId do

tests/lean/unfoldDefEq.lean

@@ -6,4 +6,12 @@ def some_property {n} (x : Fin n) : Prop :=
 
 example (x : (Wrapper n).1) (h : some_property x) : True := by
   unfold Wrapper at x
-  done
+  trace_state
+  simp at x
+  trace_state
+  sorry
+
+example (x : (Wrapper n).1) (h : some_property x) : True := by
+  simp [Wrapper] at x
+  trace_state
+  sorry

tests/lean/unfoldDefEq.lean.expected.out

@@ -1,5 +1,14 @@
-unfoldDefEq.lean:9:2-9:6: error: unsolved goals
+unfoldDefEq.lean:12:2-12:7: warning: declaration uses 'sorry'
 n : Nat
 x : (Fin n, Fin n).fst
 h : some_property x
 ⊢ True
+n : Nat
+x : Fin n
+h : some_property x
+⊢ True
+unfoldDefEq.lean:17:2-17:7: warning: declaration uses 'sorry'
+n : Nat
+x : Fin n
+h : some_property x
+⊢ True