# Documentation

Mathlib.Util.SynthesizeUsing

# SynthesizeUsing#

This is a slight simplification of the solve_aux tactic in Lean3.

def synthesizeUsing (type : Lean.Expr) (tac : ) :

synthesizeUsing type tac synthesizes an element of type using tactic tac.

The tactic tac may leave goals open, these remain as metavariables in the returned expression.

Equations
• One or more equations did not get rendered due to their size.