mul_comm fails

Stream: new members

[Hank]

The last line fails. I have tried rw mul_comm as well, but it always says the tactic failed.

import data.real.basic
variables a b : ℝ

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 rw add_assoc
  ... = a*a + (b*a + a*b + b*b) : by rw add_assoc
  ... = a*a + (a*b + a*b + b*b) : by rw ←mul_comm b*a /- ?? -/

[Patrick Johnson]

rw ←mul_comm b a

[Andrew Yang]

You should give mul_comm the two variables separately, namely rw ← mul_comm b a

[Hank]

thank you!