Algebra.Quandle held up by group

Stream: mathlib4

[zbatt]

In Algebra.Quandle there is a particularly nasty goal x * (y * z * y⁻¹) * x⁻¹ = x * y * x⁻¹ * (x * z * x⁻¹) * (x * y * x⁻¹)⁻¹ which was done in mathlib3 via the group tactic. Does it make more sense to try to "force" this to work, or write the group tactic first? (I want to know more about tactic writing and group doesn't seem to complex so I would be more than willing to try my hand at it)

[Mario Carneiro]

does simp [mul_assoc] work?

[zbatt]

ah yes!

[Kevin Buzzard]

That's pretty much the definition of group anyway ;-)

[zbatt]

that would make sense haha