mathlib

fe7b407f - feat(tactic/explode): display exploded proofs as widgets (#4718)

feat(tactic/explode): display exploded proofs as widgets (#4718) #4094. This is a more advanced version of the expandable `#explode` diagram implemented in the [Mathematica-Lean Link](http://robertylewis.com/leanmm/lean_mm.pdf). The widget adds features such as jumping to definitions and exploding constants occurring in a proof term subsequently. Note that right now the [\<details\>](https://developer.mozilla.org/en-US/docs/Web/HTML/Element/details) tag simply hides the information. "Exploding on request" requires a bit more refactoring on `#explode` itself and is still on the way. Example usage:`#explode_widget iff_true_intro`.