feat: "try this" messages with support for interactivity#10524

mhuisi merged 4 commits intoleanprover:masterleanprover/lean4:masterfrom

mhuisi:mhuisi/show-term-regressionmhuisi/lean4:mhuisi/show-term-regressionCopy head branch name to clipboard