∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι]
  {s : Finset κ} {t : κ → Finset ι}, (s.biUnion fun k => {i ∈ t k | f i ≠ 0}) = {i ∈ s.biUnion t | ¬f i = 0}