`SynthesizeUsing`

#

This is a slight simplification of the `solve_aux`

tactic in Lean3.

`synthesizeUsing type tac`

synthesizes an element of type `type`

using tactic `tac`

.

The tactic `tac`

is allowed to leave goals open, and these remain as metavariables in the
returned expression.

## Instances For

`synthesizeUsing type tac`

synthesizes an element of type `type`

using tactic `tac`

.

The tactic must solve for all goals, in contrast to `synthesizeUsing`

.

## Instances For

`synthesizeUsing type tacticSyntax`

synthesizes an element of type `type`

by evaluating the
given tactic syntax.

Example:

```
let (gs, e) ← synthesizeUsingTactic ty (← `(tactic| congr!))
```

The tactic `tac`

is allowed to leave goals open, and these remain as metavariables in the
returned expression.

## Instances For

`synthesizeUsing' type tacticSyntax`

synthesizes an element of type `type`

by evaluating the
given tactic syntax.

Example:

```
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)
```