feat: add sym => interactive mode

[leodemoura]

This PR adds a sym => tactic that enters an interactive symbolic simulation
mode built on grind. Unlike grind =>, it does not eagerly introduce
hypotheses or apply by-contradiction, giving users explicit control over
intro, apply, and internalize steps.

New tactics available in sym => mode:

• intro / intros: introduce binders and internalize into the E-graph by
  default. Use intro~ or intro (internalize := false) to skip
  internalization.
• apply t: apply backward rules with caching for repeat.
• internalize / internalize_all: internalize hypotheses into the E-graph.
• by_contra: apply proof by contradiction, negating the target.

Satellite solvers (lia, ring, linarith) automatically introduce remaining
binders and apply by-contradiction in sym => mode, matching their behavior in
default tactic mode. All existing grind => tactics (finish, instantiate,
cases, etc.) also work in sym => mode. The sym-specific tactics are guarded
and rejected in regular grind => mode.

example (x : Nat) : myP x → myQ x := by
  sym [myP_myQ] =>
    intro h
    finish

example (x y z : Nat) : x > 1 → x + y + z > 0 := by
  sym =>
    lia

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ea49bc9bcf41591e02e66313e5108159152e9df5 --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 15:05:48)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase ea49bc9bcf41591e02e66313e5108159152e9df5 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-18 15:05:49)