Info View without separate window

[ultronozm]

It can be useful to see the goal state without having the dedicated Lean Goal buffer visible (which has the further disadvantage of being shared by all lean4 buffers). I've been doing so using overlays in my fork https://github.com/ultronozm/lean4-mode with the package https://github.com/ultronozm/czm-lean4.el (via the commands czm-lean4-toggle-goal-overlay and czm-lean4-live-goal-mode). It looks like the attached image. I'd be happy to try to help contribute some version of this.

The proposal is not to dispense with the goal buffer altogether, but instead to explore more flexible ways of reporting the goal.