RubiksCube , needs Help.

Stream: Is there code for X?

[chenjulang]

Check this repository and mainly these two files : https://github.com/chenjulang/rubikcubegroup
rubikcubegroup/RubiksCube
/RubiksCubeFunc.lean
rubikcubegroup/RubiksCube
/FuncProofs.lean

I'm proving "valid_reachable" and "Thistlethwaite's Algorithm" and so many related lemmas recently.
Any advise would be appreciated, because i'm not good at Lean4 Language. :)

[chenjulang]

The project originates from https://github.com/AlexDuchnowski/rubiks-cube