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

State before:
ι : Type u_1
n : ℕ
inst✝ : DecidableEq ι
f : ι → 𝔽₂X
S✝ : Finset ι
i : ι
S : Finset ι
h : i ∉ S
h0 : XpowMul n (S.sum f) = ∑ i ∈ S, XpowMul n (f i)
⊢ XpowMul n ((insert i S).sum f) = ∑ i ∈ insert i S, XpowMul n (f i)
Tactic:
rw [Finset.sum_insert h, Finset.sum_insert h, XpowMul_𝔽₂X_add, h0]
State after:
no goals