mathlib

6bed7d4f - fix(tactic/interactive): issue where long term tooltips break layout (#4882)

fix(tactic/interactive): issue where long term tooltips break layout (#4882) For issue description see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/widget.20v.20long.20term.20names Basically the problem is that if the little 'argument pills' in the tooltip are too long, then there is a fight between the expression linebreaking algorithm and the pill linebreaking algorithm and something gets messed up. A first attempt to fix this is to use flexbox for laying out the pills. Still some issues with expressions linebreaking weirdly to sort out before this should be pulled. Need to find a mwe that I can put in a file without a huge dependency tree.