substitute a term

Stream: general

[Siyuan Yan]

hi, learner of lean here. How do I use the equality gg in g?

▶ 1 goal
a b c : ℝ
g : c * b * a = c * (b * a)
gg : b * a = a * b
⊢ c * b * a = b * (a * c)

[Mario Carneiro]

It doesn't directly apply since the term is associated wrong actually it does apply

[Mario Carneiro]

you can do rw [gg] at g

[Siyuan Yan]

Mario Carneiro said:

you can do rw [gg] at g

thanks! I did rw gg at g and it worked too. Why was the brackets?

[Mario Carneiro]

the brackets are optional when there is only one thing