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

State before:
m n : ℕ
P : 𝔽₂X
⊢ XpowMul (m + n) P = XpowMul n (XpowMul m P)
Tactic:
unfold XpowMul
State after:
m n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun k => k + (m + n)) P.toFinset } =
    { toFinset := Finset.image (fun k => k + n) { toFinset := Finset.image (fun k => k + m) P.toFinset }.toFinset }

State before:
m n : ℕ
P : 𝔽₂X
⊢ { toFinset := Finset.image (fun k => k + (m + n)) P.toFinset } =
    { toFinset := Finset.image (fun k => k + n) { toFinset := Finset.image (fun k => k + m) P.toFinset }.toFinset }
Tactic:
rw [𝔽₂X.ext_iff, eq_comm, Finset.image_image, comp_add_right]
State after:
no goals