M : Type ?u.27284
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
⊢ ∀ (l : List R) [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
M : Type ?u.27284
inst✝³ : Zero M
l✝ : List M
inst✝² : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝¹ : AddMonoid R
l : List R
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
⊢ toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
revert l
M : Type ?u.27284
inst✝² : Zero M
l✝ : List M
inst✝¹ : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
l : List R
⊢ ∀ [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
M : Type ?u.27284
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
⊢ ∀ (l : List R) [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
intro l
no goals
M : Type ?u.27284
inst✝² : Zero M
l✝ : List M
inst✝¹ : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
l : List R
⊢ ∀ [inst : DecidablePred fun x => getD l x 0 ≠ 0],
    toFinsupp l = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum l))
induction l using List.reverseRecOn with
| H0 => exact toFinsupp_nil
| H1 x xs ih =>
  classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
no goals
case H0
M : Type ?u.27284
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x => getD [] x 0 ≠ 0],
    toFinsupp [] = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum []))
exact toFinsupp_nil
no goals
case H1
M : Type ?u.27284
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
x : List R
xs : R
ih :
  ∀ [inst : DecidablePred fun x_1 => getD x x_1 0 ≠ 0],
    toFinsupp x = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum x))
⊢ ∀ [inst : DecidablePred fun x_1 => getD (x ++ [xs]) x_1 0 ≠ 0],
    toFinsupp (x ++ [xs]) = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum (x ++ [xs])))
classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
no goals
case H1
M : Type ?u.27284
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
inst✝ : AddMonoid R
x : List R
xs : R
ih :
  ∀ [inst : DecidablePred fun x_1 => getD x x_1 0 ≠ 0],
    toFinsupp x = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum x))
⊢ ∀ [inst : DecidablePred fun x_1 => getD (x ++ [xs]) x_1 0 ≠ 0],
    toFinsupp (x ++ [xs]) = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum (x ++ [xs])))
simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]