Flipping an equality

Stream: new members

[Omnikar]

Hi, I just found out about Lean recently and have been reading through and following along with "Theorem Proving with Lean 4." I've come here to ask: given hab : a = b, how would I obtain hba : b = a?

[Omnikar]

Oh, I found the answer, it's Eq.symm

[Kevin Buzzard]

You can probably even use hab.symm because of dot notation