chore: fix superfluous lemmas in simp.trace

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

@@ -37,13 +37,18 @@ def synthesizeArgs (thmId : Origin) (xs : Array Expr) (bis : Array BinderInfo) (
         if (← synthesizeInstance x type) then
           continue
       if (← isProp type) then
+        -- We save the state, so that `UsedTheorems` does not accumulate
+        -- `simp` lemmas used during unsuccessful discharging.
+        let usedTheorems := (← get).usedTheorems
         match (← discharge? type) with
         | some proof =>
           unless (← isDefEq x proof) do
             trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to assign proof{indentExpr type}"
+            modify fun s => { s with usedTheorems }
             return false
         | none =>
           trace[Meta.Tactic.simp.discharge] "{← ppOrigin thmId}, failed to discharge hypotheses{indentExpr type}"
+          modify fun s => { s with usedTheorems }
           return false
   return true
 where

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

@@ -45,9 +45,15 @@ structure State where
 
 abbrev SimpM := ReaderT Context $ StateRefT State MetaM
 
+structure SavedState where
+  meta : Meta.SavedState
+  usedTheorems : UsedSimps
+
 instance : MonadBacktrack SavedState SimpM where
-  saveState      := Meta.saveState
-  restoreState s := s.restore
+  saveState      := return ⟨← Meta.saveState, (← get).usedTheorems⟩
+  restoreState s := do
+    s.meta.restore
+    modify fun t => { t with usedTheorems := s.usedTheorems }
 
 inductive Step where
   | visit : Result → Step

tests/lean/simp_trace_backtrack.lean

@@ -0,0 +1,19 @@
+-- As reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.3F.20giving.20nonsense.20lemmas/near/403082483
+
+universe u
+
+-- {α : Type} works as expected, as does specializing this lemma for `Nat`.
+@[simp]
+theorem tsub_eq_zero_of_le {α : Type u} [LE α] [Sub α] [OfNat α 0] {a b : α} :
+    a ≤ b → a - b = 0 := by sorry
+
+@[simp]
+theorem ge_iff_le (x y : Nat) : x ≥ y ↔ y ≤ x := Iff.rfl
+
+set_option tactic.simp.trace true
+
+-- This used to report: `Try this: simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub]`
+-- because we were not backtracking the "used simps" when the discharger failed.
+example {n : Nat} : n = 2 - (n + 1) := by
+  simp [Nat.succ_sub_succ_eq_sub]
+  sorry

tests/lean/simp_trace_backtrack.lean.expected.out

@@ -0,0 +1,3 @@
+simp_trace_backtrack.lean:7:8-7:26: warning: declaration uses 'sorry'
+Try this: simp only [Nat.succ_sub_succ_eq_sub]
+simp_trace_backtrack.lean:17:0-17:7: warning: declaration uses 'sorry'