SynthesizeUsing
#
This is a slight simplification of the solve_aux
tactic in Lean3.
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.