Tic-tac-toe meets Lean 4

Some of the definitions remind me of the formalisation I wrote for the game Havannah by Christian Freeling. See https://iwriteiam.nl/Havannah.html Maybe I should try to write it in Lean as well.