∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∉ s →
      ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 insert a s), f t =
        ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t + ∑ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f (insert a t)