I guess I don't understand nth_rewrite

I've been fighting against nth_rewrite for quite some time, and I don't understand what I'm doing wrong. For example, in the "Power World", level 7/10 (i.e. proving mul_pow), I currently have:

(a * b) ^ succ c = a ^ succ c * b ^ succ c

I would expect that applying nth_rewrite 1 [pow_succ] to this would result in (a * b) ^ c * (a * b) = a ^ succ c * b ^ succ c, and in fact it does.

I would furthermore expect that applying nth_rewrite 2 [pow_succ] to the same original line would result in (a * b) ^ succ c = (a ^ c * a) * b ^ succ c, and that applying nth_rewrite 3 [pow_succ] would result in (a * b) ^ succ c = a ^ succ c * (b ^ c * b). But neither of these do what I expect; instead they throw errors. For example:

To be clear, I've been having this sort of problem with nth_rewrite frequently, not just in the case of this particular example. Am I doing something incorrectly? If so, what? Thanks in advance.

leanprover-community / lean4game

I guess I don't understand nth_rewrite #141