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

State before:
i : ℕ
S : Finset ℕ
h : i ∉ S
h0 : S.sum Xpow = ofFinset S
⊢ (insert i S).sum Xpow = ofFinset (insert i S)
Tactic:
rw [Finset.sum_insert h, h0]
State after:
i : ℕ
S : Finset ℕ
h : i ∉ S
h0 : S.sum Xpow = ofFinset S
⊢ Xpow i + ofFinset S = ofFinset (insert i S)

State before:
i : ℕ
S : Finset ℕ
h : i ∉ S
h0 : S.sum Xpow = ofFinset S
⊢ Xpow i + ofFinset S = ofFinset (insert i S)
Tactic:
exact 𝔽₂X.ext _ _ (symmDiff_singleton_eq_insert h)
State after:
no goals