The final step to a tutorial is to match both LHS and RHS since a*b is not the same as b*a according to the rules of the LEAN programing. The Goal is given below.
Goal: a ^ d * b ^ d * a * b = a ^ d * a * b ^ d * b
Is there a faster way to swap b ^ d * a to match the RHS? With the invisible brackets the statement actually looks like: ((a ^ d * b ^ d) * a )* b,
The long way to this is to massage the brackets to (a ^ d * (b ^ d * a) * b) before using[mul_col] and then repeated [mul_assoc] to push the brackets to match on both sides.