perf: avoid instantiating `grind` proofs at every case split

This PR speeds up `grind` on goals with many nested case splits. Building the proof of a case split no longer traverses the proofs of the case splits below it.

`grind`'s own time compared to master:
* `tests/elab_bench/lia_case_splits.lean`: 3.6 s → 1.6 s.
* `lia` on a sum of 13 terms `if cᵢ then xᵢ else 0`: 8.9 s → 3.7 s.
* `grind` on `x = 0 ∨ … ∨ x = 999` with `1010 ≤ x`: 180 s → 23 s.

Each case split instantiated its proof, whose delayed assignments are not cached, so every enclosing case split traversed the whole subproof again. Now `getProofInfo` summarizes a proof without instantiating it: its free variables, whether it contains a synthetic `sorry`, and whether it contains an unassigned metavariable of `grind`'s depth (e.g., an open subgoal after an interactive `cases_next`). Complete summaries are cached per metavariable. `getFalseProof?` and `mkHoistedDecls` use it instead of instantiating, and `mkHoistedDecls` abstracts the hoisted declarations with a delayed assignment, as `intro` does.

Non-chronological backtracking now also applies when the goal contains metavariables created before `grind`, whose delayed assignments `instantiateMVars` does not resolve.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>