feat: `show` tactic (full version)

[digama0]

This implements the TODO in the show tactic: show e will first try to change the goal to e, and if that doesn't work it will try to change one of the other open goals to e and select it. Note: This implementation allows the goal to change in a non-defeq way and will insert coercions. I plan to follow this up with an implementation of change which is only for strictly defeq changes, similar to dsimp only.

A thought: should the goal-selecting version of show be spelled show e => tac instead? It is a bit awkward that it acts like a move-to-front tactic but has no case => form so you have to do show e; . tac to actually work on the selected goal.

[gebner]

should the goal-selecting version of show be spelled show e => tac instead?

👍

[leodemoura]

Dev meeting summary: make Lean 4 show compatible with Lean 3 show.