The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to human

The algebra was tedious because for example, the very second thing you prove in the tutorial is that addition is associative. If you were teaching this to humans you would then immediately tell them that you now can omit parentheses because you have an algorithm to re-parenthesize however you want. But instead, for entire rest of the tutorial, you had to manually rewrite every single parenthesis yourself (with syntax that is pretty unergonomic for doing so too). I guess I found it a little disappointing that it's not easy to instruct it on how to fill in gaps so you can skip steps the same way you would in a human proof (which would only need a note saying that you're using associativity and parens are omitted thereafter, and any human reader will accept that as valid)