mathlib

a17a9a6a - fix(tactic/{use,ring}): instantiate metavariables in goal (#1520)

fix(tactic/{use,ring}): instantiate metavariables in goal (#1520) `use` now tidies up the subgoals that it leaves behind after instantiating constructors. `ring` is sensitive to the presence of such metavariables, and we can't guarantee that it doesn't see any, so it should check for them before it runs.