Proving `succ_mul` without using `nth_rewrite`

Question

I'm trying level 3 in the multiplication world of the Natural Number Game.

My proof is given below, but I am not satisfied with it since it uses nth_rewrite.

This is the first exercise where I've needed to use nth_rewrite, and that tactic isn't really described in the help text for the exercise, it merely isn't prohibited.

Basically, at some point I ended up with this proof state. From here, it's clear what you need to do, you need to apply associativity of addition to make n + a on the LHS into an actual term, apply commutativity, and then unapply associativity.

However, you need to use nth_rewrite when applying commutativity of addition because you are actually interested in the second expression headed up by a plus sign.

// This is the proof state where using nth_rewrite feels natural

Current Goal
Objects:
an: ℕ
Assumptions:
n_ih: succ a * n = a * n + n
Goal:
succ (a * n + n + a) = succ (a * n + a + n)

That got me wondering how you can prove this without using nth_rewrite.

Here's the full proof script.

theorem succ_mul (a b : ℕ) : succ a * b = a * b + b := by
induction b
rw [add_zero]
rw [mul_zero]
rw [mul_zero]
rfl
repeat rw [mul_succ]
rw [n_ih]
repeat rw [add_succ]
repeat rw [add_succ]
rw [add_assoc]
nth_rewrite 2 [add_comm]
rw [<- add_assoc]
rfl

Answer 1

You can just look at the "official" proof in the NNG4 github repo; it doesn't use nth_rewrite but it does use add_right_comm.

Answer 2

Outside of the NNG, I use the conv tactic for that. Especially conv in pattern => rw [...] form. It is super useful in my limited experience.