Theorem: IMOSL.IMO2012A5.ℤφ.mul_comm (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/Zphi.lean)

State before:
a b a' b' : ℤ
⊢ { re := a, im := b } * { re := a', im := b' } = { re := a', im := b' } * { re := a, im := b }
Tactic:
rw [mul_def, mul_def, mul_comm a, mul_comm b, add_comm (a * b')]
State after:
no goals