Documentation

Mathlib.Util.SynthesizeUsing

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.