Theorem: IMOSL.IMO2012A5.ℤ₄.add_mul (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/Z4.lean)

State before:
x y z : ℤ₄
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [ℤ₄.mul_comm, ℤ₄.mul_add, z.mul_comm, z.mul_comm]
State after:
no goals