[GOAL]
M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ n : ℕ
⊢ n ∈ Finset.filter (fun i => getD l i 0 ≠ 0) (Finset.range (length l)) ↔ (fun i => getD l i 0) n ≠ 0
[PROOFSTEP]
simp only [Ne.def, Finset.mem_filter, Finset.mem_range, and_iff_right_iff_imp]
[GOAL]
M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ n : ℕ
⊢ ¬getD l n 0 = 0 → n < length l
[PROOFSTEP]
contrapose!
[GOAL]
M : Type u_1
inst✝¹ : Zero M
l : List M
inst✝ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ n : ℕ
⊢ length l ≤ n → getD l n 0 = 0
[PROOFSTEP]
exact getD_eq_default _ _
[GOAL]
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
⊢ toFinsupp [] = 0
[PROOFSTEP]
ext
[GOAL]
case h
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
inst✝ : DecidablePred fun i => getD [] i 0 ≠ 0
a✝ : ℕ
⊢ ↑(toFinsupp []) a✝ = ↑0 a✝
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
ext ⟨_ | i⟩
[GOAL]
case h.zero
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]) Nat.zero = ↑(Finsupp.single 0 x) Nat.zero
[PROOFSTEP]
simp [Finsupp.single_apply, (Nat.zero_lt_succ _).ne]
[GOAL]
case h.succ
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
n✝ : ℕ
⊢ ↑(toFinsupp [x]) (Nat.succ n✝) = ↑(Finsupp.single 0 x) (Nat.succ n✝)
[PROOFSTEP]
simp [Finsupp.single_apply, (Nat.zero_lt_succ _).ne]
[GOAL]
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
⊢ toFinsupp (l₁ ++ l₂) = toFinsupp l₁ + Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)
[PROOFSTEP]
ext n
[GOAL]
case h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
⊢ ↑(toFinsupp (l₁ ++ l₂)) n = ↑(toFinsupp l₁ + Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
simp only [toFinsupp_apply, Finsupp.add_apply]
[GOAL]
case h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
cases lt_or_le n l₁.length with
| inl h =>
  rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
  rintro ⟨k, rfl : length l₁ + k = n⟩
  exact h.not_le (self_le_add_right _ _)
| inr h =>
  rcases exists_add_of_le h with ⟨k, rfl⟩
  rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
  exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
case h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
x✝ : n < length l₁ ∨ length l₁ ≤ n
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
cases lt_or_le n l₁.length with
| inl h =>
  rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
  rintro ⟨k, rfl : length l₁ + k = n⟩
  exact h.not_le (self_le_add_right _ _)
| inr h =>
  rcases exists_add_of_le h with ⟨k, rfl⟩
  rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
  exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
case h.inl
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : n < length l₁
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]

| inl h =>
  rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
  rintro ⟨k, rfl : length l₁ + k = n⟩
  exact h.not_le (self_le_add_right _ _)
[GOAL]
case h.inl
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : n < length l₁
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
[GOAL]
case h.inl.h
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : n < length l₁
⊢ ¬n ∈ Set.range ↑(addLeftEmbedding (length l₁))
[PROOFSTEP]
rintro ⟨k, rfl : length l₁ + k = n⟩
[GOAL]
case h.inl.h.intro
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
k : ℕ
h : length l₁ + k < length l₁
⊢ False
[PROOFSTEP]
exact h.not_le (self_le_add_right _ _)
[GOAL]
case h.inr
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : length l₁ ≤ n
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]

| inr h =>
  rcases exists_add_of_le h with ⟨k, rfl⟩
  rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
  exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
case h.inr
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
n : ℕ
h : length l₁ ≤ n
⊢ getD (l₁ ++ l₂) n 0 = getD l₁ n 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) n
[PROOFSTEP]
rcases exists_add_of_le h with ⟨k, rfl⟩
[GOAL]
case h.inr.intro
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
k : ℕ
h : length l₁ ≤ length l₁ + k
⊢ getD (l₁ ++ l₂) (length l₁ + k) 0 =
    getD l₁ (length l₁ + k) 0 + ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) (length l₁ + k)
[PROOFSTEP]
rw [getD_append_right _ _ _ _ h, add_tsub_cancel_left, getD_eq_default _ _ h, zero_add]
[GOAL]
case h.inr.intro
M : Type u_1
inst✝⁵ : Zero M
l : List M
inst✝⁴ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x => getD (l₁ ++ l₂) x 0 ≠ 0
inst✝¹ : DecidablePred fun x => getD l₁ x 0 ≠ 0
inst✝ : DecidablePred fun x => getD l₂ x 0 ≠ 0
k : ℕ
h : length l₁ ≤ length l₁ + k
⊢ getD l₂ k 0 = ↑(Finsupp.embDomain (addLeftEmbedding (length l₁)) (toFinsupp l₂)) (length l₁ + k)
[PROOFSTEP]
exact Eq.symm (Finsupp.embDomain_apply _ _ _)
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ toFinsupp (x :: xs) =
    Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } (toFinsupp xs)
[PROOFSTEP]
classical
convert toFinsupp_append [x] xs using 3
· exact (toFinsupp_singleton x).symm
· ext n
  exact add_comm n 1
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ toFinsupp (x :: xs) =
    Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } (toFinsupp xs)
[PROOFSTEP]
convert toFinsupp_append [x] xs using 3
[GOAL]
case h.e'_3.h.e'_5
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ Finsupp.single 0 x = toFinsupp [x]
[PROOFSTEP]
exact (toFinsupp_singleton x).symm
[GOAL]
case h.e'_3.h.e'_6.h.e'_5
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
⊢ { toFun := Nat.succ, inj' := Nat.succ_injective } = addLeftEmbedding (length [x])
[PROOFSTEP]
ext n
[GOAL]
case h.e'_3.h.e'_6.h.e'_5.h
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => getD (x :: xs) x_1 0 ≠ 0
inst✝ : DecidablePred fun x => getD xs x 0 ≠ 0
n : ℕ
⊢ ↑{ toFun := Nat.succ, inj' := Nat.succ_injective } n = ↑(addLeftEmbedding (length [x])) n
[PROOFSTEP]
exact add_comm n 1
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i => getD (xs ++ [x]) i 0 ≠ 0
inst✝ : DecidablePred fun i => getD xs i 0 ≠ 0
⊢ toFinsupp (xs ++ [x]) = toFinsupp xs + Finsupp.single (length xs) x
[PROOFSTEP]
classical rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single, addLeftEmbedding_apply, add_zero]
[GOAL]
M : Type u_1
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun i => getD (xs ++ [x]) i 0 ≠ 0
inst✝ : DecidablePred fun i => getD xs i 0 ≠ 0
⊢ toFinsupp (xs ++ [x]) = toFinsupp xs + Finsupp.single (length xs) x
[PROOFSTEP]
rw [toFinsupp_append, toFinsupp_singleton, Finsupp.embDomain_single, addLeftEmbedding_apply, add_zero]
[GOAL]
M : Type u_1
inst✝³ : Zero M
l✝ : List M
inst✝² : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_2
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))
[PROOFSTEP]
revert l
[GOAL]
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
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))
[PROOFSTEP]
intro l
[GOAL]
M : Type u_1
inst✝² : Zero M
l✝ : List M
inst✝¹ : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_2
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))
[PROOFSTEP]
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]
[GOAL]
M : Type u_1
inst✝² : Zero M
l✝ : List M
inst✝¹ : DecidablePred fun x => getD l✝ x 0 ≠ 0
n : ℕ
R : Type u_2
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))
[PROOFSTEP]
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]
[GOAL]
case H0
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x => getD [] x 0 ≠ 0],
    toFinsupp [] = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum []))
[PROOFSTEP]

| H0 => exact toFinsupp_nil
[GOAL]
case H0
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
inst✝ : AddMonoid R
⊢ ∀ [inst : DecidablePred fun x => getD [] x 0 ≠ 0],
    toFinsupp [] = sum (map (fun nr => Finsupp.single nr.fst nr.snd) (enum []))
[PROOFSTEP]
exact toFinsupp_nil
[GOAL]
case H1
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
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])))
[PROOFSTEP]

| H1 x xs ih => classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
[GOAL]
case H1
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
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])))
[PROOFSTEP]
classical simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
[GOAL]
case H1
M : Type u_1
inst✝² : Zero M
l : List M
inst✝¹ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_2
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])))
[PROOFSTEP]
simp [toFinsupp_concat_eq_toFinsupp_add_single, enum_append, ih]
