simple rw issue

Stream: new members

[Alfredo Garcia]

Hey, i have a simple rw issue but i can't figure out what is it. i have some demo code at https://leanprover-community.github.io/lean-web-editor/#code=import%20data.zmod.basic%0A%0A--%20don't%20work%0Alemma%20testing%20%28x%20a%20%3A%20zmod%206%29%20%28h%20%3A%20a.val.gcd%206%20%3D%201%29%3A%20x%20*%20a%20*%20a%E2%81%BB%C2%B9%20%3D%20x%20%3A%3D%0Abegin%0A%20%20rw%20zmod.mul_inv_eq_gcd%2C%0Aend%0A%0A--%20work%0Alemma%20testing2%20%28a%20%3A%20zmod%206%29%20%28h%20%3A%20a.val.gcd%206%20%3D%201%29%3A%20a%20*%20a%E2%81%BB%C2%B9%20%3D%201%20%3A%3D%0Abegin%0A%20%20rw%20zmod.mul_inv_eq_gcd%2C%0A%20%20finish%2C%0Aend

[Alfredo Garcia]

any hint is appreciated

[Reid Barton]

x * a * a⁻¹ means (x * a) * a⁻¹. You can rewrite with mul_assoc to move the a * a⁻¹ together.

[Alfredo Garcia]

perfect, i knew it was something dumb, thanks for the help