no goals
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
x : M
inst✝ : DecidablePred fun x_1 => getD [x] x_1 0 ≠ 0
⊢ toFinsupp [x] = Finsupp.single 0 x
ext ⟨_ | i⟩ <;> simp [Finsupp.single_apply, (Nat.zero_lt_succ _).ne]