chore(*): import expression widgets from core (#3181)
With widgets, the rendering of the tactic state is implemented in pure Lean code. I would like to move this part (temporarily) into mathlib to facilitate collaborative improvement and rapid iteration under a mature community review procedure. (That is, I want other people to tweak it themselves without having to wait a week for the next Lean release to see the effect.)
I didn't need to change anything in the source code (except for adding some doc strings). So it should be easy to copy it back to core if we want to.
There are no changes required to core for this PR.
Co-authored-by: E.W.Ayers <E.W.Ayers@maths.cam.ac.uk>
