Theorem: IMOSL.IMO2012A5.𝔽₄.add_mul (IMOSLLean4/IMO2012/A5/Extra/ExplicitRings/F4.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