Lean metaprogramming: no `Quote Int` instance; splice ℤ data via toExpr

On Lean/Mathlib v4.35.0, #synth Lean.Quote ℤ and #synth Quote (List ℤ) both fail, while Quote (List Nat) exists. So quote cannot turn computed integer data into syntax for a tactic quotation. ToExpr (List Int) does exist, so ← Term.exprToSyntax (toExpr l) gives a term you can splice as $xS. A gotcha when you combine this with goal manipulation: exprToSyntax creates a metavariable in the *current* local context. After MVarId.intro plus replaceMainGoal, an outer withMainContext still refers to the old goal, and spliced fvars then fail with 'unknown free variable _fvar.N'. Wrap the call as withMainContext <| Term.exprToSyntax ... after changing goals.