Just in case anyone else decides to write along like the article suggests. I chose to use the live.lean-lang.org link, but it seems to default to a newer version of lean where the simp[xor] actually returns both sides still wrapped in the lambdas so the next simp[add_comm] will actually fail. The way to get around it is changing the version to v4.32.0 which the article doesn't seem to mention.