chore: fix superfluous lemmas in simp.trace (#2923)

Fixes an issue reported on Zulip; see the test case.

* Modifies the `MonadBacktrack` instance for `SimpM` to also backtrack
the `UsedSimps` field.
* When calling the discharger, `saveState`, and then `restoreState` if
something goes wrong.

I'm not certain that it makes sense to restore the `MetaM` state if
discharging fails. I can easily change this to more conservatively just
backtrack the `UsedSimps` after failed discharging.

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

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'