add_assoc fail

Stream: new members

[Hank]

In the following code

example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b :=
calc
(a + b) * (a + b)
= (a + b) * a + (a + b) * b : by rw mul_add
... = (a * a + b * a) + (a + b) * b : by rw add_mul
... = a * a + b * a + (a * b + b * b) : by rw add_mul
... = a * a + (b * a + (a * b + b * b)) : by add_assoc
... =

lean does not accept add_assoc as a workable tactic in the last line. But I am using x + y + z = x + (y + z) with x=aa, y=ba, and z=ab+bb

[Alex J. Best]

docs#add_assoc isn't a tactic, it's a lemma, so you need to do by rw add_assoc

[Alex J. Best]

Also #backticks will make it easier for people to try your code out

[Hank]

thank you! that works