fix: simp? should track unfolded let-decls

closes #3501

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

@@ -76,9 +76,11 @@ private def reduceProjFn? (e : Expr) : SimpM (Option Expr) := do
         -- `structure` projections
         reduceProjCont? (← unfoldDefinition? e)
 
-private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : MetaM Expr := do
+private def reduceFVar (cfg : Config) (thms : SimpTheoremsArray) (e : Expr) : SimpM Expr := do
   let localDecl ← getFVarLocalDecl e
   if cfg.zetaDelta || thms.isLetDeclToUnfold e.fvarId! || localDecl.isImplementationDetail then
+    if !cfg.zetaDelta && thms.isLetDeclToUnfold e.fvarId! then
+      recordSimpTheorem (.fvar localDecl.fvarId)
     let some v := localDecl.value? | return e
     return v
   else

tests/lean/run/3501.lean

@@ -0,0 +1,9 @@
+/-- info: Try this: simp only [Nat.reduceMul, a] -/
+#guard_msgs in
+example : True := by
+  let a := 10
+  have : a * 2 = 10 * 2 := by
+    simp [a]
+  have : a * 2 = 10 * 2 := by
+    simp? [a] -- should say simp only [Nat.reduceMul, a]
+  trivial