mathlib

77f3fa47 - feat(tactic/interactive_expr): add copy button to type tooltip (#3633)

feat(tactic/interactive_expr): add copy button to type tooltip (#3633) There should now be a 'copy expression' button in each tooltip which can be used to copy the current expression to the clipboard.  I have not tested on windows yet. Also broke out `widget_override.goals_accomplished_message` so that users can override it. For example: ``` meta def my_new_msg {α : Type} : widget.html α := "my message" attribute [vm_override my_new_msg] widget_override.goals_accomplished_message ``` Co-authored-by: Ed Ayers <EdAyers@users.noreply.github.com>