Natural number game 7/10 mul_pow

Stream: new members

[Moti Ben-Ari]

At the follow state of this game:
mul_pow.jpg
I want to use associativity and commutatively work:

rw [mul_assoc a^x a (b^x * b)]
rw [mul_comm b^x b]

even though that seems be what the "Targetted usage" is suggesting. I get tactic 'rewrite' failed, equality or iff proof expected, but writing the (long) equality I want doesn't work either. The "rules" of the game seem to indicate that this should be provable using only the tactics and theorems in the menu on the right.

[Ruben Van de Velde]

Try rw [mul_assoc (a ^ x) a (b^x * b)]

[Moti Ben-Ari]

Thanks @Ruben Van de Velde , I finished this game.

The need for parentheses goes against my intuition from experience. What exactly is the syntactically rule here (and where can I find it)?