∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι) (b : β i)
  [inst_3 : Decidable (b = 0)],
  (f.update i b).support = if b = 0 then (DFinsupp.erase i f).support else insert i f.support