chore: remove unused MonadBacktrack instance for SimpM (#2943)

We noticed at
https://github.com/leanprover/lean4/pull/2923#discussion_r1400468371
that this instance is not used. It's arguably also incorrect (as it
doesn't backtrack the `usedTheorems` field).

Seems better to just remove to avoid confusion.

Evidence that this is dead code:
* After deleting the instance, calling `saveState` in the `SimpM` monad
raises an error `failed to synthesize instance MonadBacktrack PUnit
SimpM`.
* Understanding the `MonadBacktrack` monad leads one to believe that
would have happened, via the fact that the only instances for
`MonadBacktrack` are either concrete instances (e.g. for `MetaM`,
`TacticM`, etc), or a single lifting instance `instance [MonadBacktrack
s m] [Monad m] : MonadBacktrack s (ExceptT ε m)`. (This is good and
correct behaviour: lifting instances for `MonadBacktrack` would be hard
to model.)
* Mathlib builds after the instance is removed.

Potential evidence that I have not sought, because we don't have
sufficient tooling:
* Compiling Lean/Std/Mathlib with a debugger, breaking on entering this
code.

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

@@ -45,10 +45,6 @@ structure State where
 
 abbrev SimpM := ReaderT Context $ StateRefT State MetaM
 
-instance : MonadBacktrack SavedState SimpM where
-  saveState      := Meta.saveState
-  restoreState s := s.restore
-
 inductive Step where
   | visit : Result → Step
   | done  : Result → Step