Lean4
/-- `synthesizeUsing' type tacticSyntax` synthesizes an element of type `type` by evaluating the
given tactic syntax.
Example:
```lean
let e ← synthesizeUsingTactic' ty (← `(tactic| norm_num))
```
The tactic must solve for all goals, in contrast to `synthesizeUsingTactic`.
If you need to insert expressions into a tactic proof, then you might use `synthesizeUsing'`
directly, since the `TacticM` monad has access to the `TermElabM` monad. For example, here
is a term elaborator that wraps the `simp at ...` tactic:
```
def simpTerm (e : Expr) : MetaM Expr := do
let mvar ← Meta.mkFreshTypeMVar
let e' ← synthesizeUsing' mvar
(do evalTactic (← `(tactic| have h := $(← Term.exprToSyntax e); simp at h; exact h)))
-- Note: `simp` does not always insert type hints, so to ensure that we get a term
-- with the simplified type (as opposed to one that is merely defeq), we should add
-- a type hint ourselves.
Meta.mkExpectedTypeHint e' mvar
elab "simpTerm% " t:term : term => do simpTerm (← Term.elabTerm t none)
```
-/
def synthesizeUsingTactic' {u : Level} (type : Q(Sort u)) (tac : Syntax) : MetaM Q($type) := do
synthesizeUsing' type
(do
evalTactic tac)
