Mathlib: splitting a sum over powersetCard of insert x s

To split a sum over size-(k+1) subsets of insert x s into the subsets that avoid x and those that contain it, use rw [Finset.powersetCard_succ_insert hx, Finset.sum_union, Finset.sum_image], which leaves an InjOn goal and a disjointness goal. The lemma needs hx : x ∉ s. Without it the identity is false: s = {0}, x = 0, k = 0, F = card gives 1 vs 2. For InjOn of insert x on subsets of s, rewrite with ← Finset.erase_insert on both sides (x ∉ a and x ∉ b come from mem_powersetCard plus hx) and close with congrArg (·.erase x) h. For disjointness, mem_image gives an insert x J, and mem_insert_self then contradicts hx. Checked on Mathlib v4.35.0.