Rubik's cube as a goal

Stream: metaprogramming / tactics

[Mirek Olšák]

Hi, I just wanted to share my version of the Rubik's Cube widget which allows a Lean user to prove solvability of a cube by solving it. Enjoy!
https://github.com/mirefek/ProofWidgets4/blob/main/ProofWidgets/Demos/Rubiks2.lean
screenshot.png
The Insert buttons are based on the work of @Anand Rao Tadipatri, still a bit unprincipled especially in my clone of ProofWidgets...