feat: finish? tactic for grind interactive mode

[leodemoura]

This PR implements the finish? tactic for the grind interactive mode. When it successfully closes the goal, it produces a code action that allows the user to close the goal using explicit grind tactic steps, i.e., without any search. It also makes explicit which solvers have been used.

This is just the first version, we will add many "bells and whistles" later. For example, instantiate steps will clearly show which theorems have been instantiated.

Example:

/--
info: Try this:
  [apply] ⏎
    cases #b0f4
    next => cases #50fc
    next => cases #50fc <;> lia
-/
#guard_msgs in
example (p : Nat → Prop) (x y z w : Int) :
    (x = 1 ∨ x = 2) →
    (w = 1 ∨ w = 4) →
    (y = 1 ∨ (∃ x : Nat, y = 3 - x ∧ p x)) →
    (z = 1 ∨ z = 0) → x + y ≤ 6 := by
  grind => finish?

The anchors in the generated script are based on stable hash codes. Moreover, users can hover over them to see the exact term used in the case split. grind? will also be implemented using the new framework.