Theorem: IMOSL.IMO2012A5.𝔽₂X.mul_assoc (IMOSLLean4/Extra/F2X/Defs.lean)

State before:
P Q : 𝔽₂X
n : ℕ
⊢ P * Q * Xpow n = P * (Q * Xpow n)
Tactic:
rw [← XpowMul_eq_mul_Xpow, ← XpowMul_eq_mul_Xpow, mul_XpowMul_right]
State after:
no goals

State before:
P Q P✝ Q✝ : 𝔽₂X
h : P * Q * P✝ = P * (Q * P✝)
h0 : P * Q * Q✝ = P * (Q * Q✝)
⊢ P * Q * (P✝ + Q✝) = P * (Q * (P✝ + Q✝))
Tactic:
rw [𝔽₂X.mul_add, 𝔽₂X.mul_add, 𝔽₂X.mul_add, h, h0]
State after:
no goals