Add hacks to tactic state display

The goal is to handle large proofs. You can now
add
`import interactive_expr`
as the last import and then
`set_option trace.filter_inst true`
or
`set_option trace.filter_inst_type true`
to permanently filter out instances or instances and types.
You also get to see the goal first to avoid scrolling.