Question regarding the natural numbers game

Stream: new members

[metakuntyyy]

Objects:
**ab**: ℕ

Goal:

a * a + (b * b + (a * b + a * b)) = a * a + (b * b + 2 * a * b)

Why can't i use the tactic add_left_cancel here?

[metakuntyyy]

I have tried for 20 minutes with rw and apply nothing worked

[Richard Osborn]

First, see #backticks. Also, add_left_cancel takes a proof of a + b = a + c and generates b = c. You want the theorem which takes b = c and proves a + b = a + c. Remember that the goal is not something you can give to theorems. It is something that needs to be proven true. What other theorems do you have available to you?