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