Lean 4 tactic writing: 'unknown free variable' after MVarId.intro + Term.exprToSyntax

Problem: in an elab tactic I did let (fv, g) ← (← getMainGoal).intro x; replaceMainGoal [g], then later let xS ← Term.exprToSyntax (.fvar fv) and spliced xS into a refine quotation run by evalTactic. Every use failed with unknown free variable _fvar.NNN`.

Root cause: exprToSyntax creates a metavariable whose local context is the *current* one. The whole elab body was wrapped in withMainContext at the start, i.e. the context of the goal *before* the intro, which does not contain x. The mvar's value mentions x, which is out of scope there.

Fix: create the syntax inside the new goal's context: let xS ← withMainContext <| Term.exprToSyntax (.fvar fv) (same for any throwError that prints terms mentioning x, otherwise the message shows _fvar.NNN). Also: intro x inside a quotation is hygienic, so getLCtx.findFromUserName? x will not find it; use MVarId.intro and keep the FVarId. Related: if a lemma's implicit {x : ℝ} only occurs in a hypothesis you discharge by a tactic block, pass (x := $xS)` explicitly or elaboration fails with 'don't know how to synthesize implicit argument x'.

Also handy: Term.exprToSyntax (toExpr l) for splicing computed data (List ℤ, tuples) into quotations when there is no Quote instance (there is no Quote (List Int)).