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