beefing up `conv_lhs`

Stream: general

[Kevin Buzzard]

I just tried (in a tactic block)

    conv_rhs {rw ← nat.choose_symm}, -- interesting failure,

and got error

    convert tactic failed, there are unsolved goals

The thing I'm rewriting needs a proof before it works. I just want that proof to pop out. I think @Eric Wieser was thinking about something related to this recently.

[Eric Wieser]

Yep, you can hack exact in there to solve the proof in place

[Eric Wieser]

abbreviation conv.interactive.exact : conv unit := tactic.interactive.exact

[Eric Wieser]

And then use exact begin ... end in the conv block

[Eric Wieser]

There's an open PR adding that one line, but I've not come back to it because it needs tests and I don't actually need it any more

[Eric Wieser]

#4615