`MetaLCtxM` and mvar depth

There seems to be some odd interaction between `MetaLCtxM` monad and meta variable depth. `lsimp` used to panic on ``` import SciLean.Tactic.CompiledTactics import SciLean.Tactic.LSimp.Elab import SciLean.Util.RewriteBy variable (i : ℕ) #check (fun x : ℕ => (if i = 0 then 1 else 0)) rewrite_by lsimp ``` This panic was fixed in [1d70152](https://github.com/lecopivo/SciLean/commit/1d7015212d7fd30904dcc28c660f9cb1c7c66238) by calling `withoutModifyingLCtx` before `withNewMCtxDepth`. I should investigate what is going on and fix `MetatLCtxM` accordingly.