case h.e'_3.h.e'_5
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
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]

case h.e'_3.h.e'_6.h.e'_5
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
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])
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
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)
convert toFinsupp_append [x] xs using 3
no goals
case h.e'_3.h.e'_5
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
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]
exact (toFinsupp_singleton x).symm
case h.e'_3.h.e'_6.h.e'_5.h
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_1
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
case h.e'_3.h.e'_6.h.e'_5
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n : ℕ
R : Type u_1
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])
ext n
no goals
case h.e'_3.h.e'_6.h.e'_5.h
M : Type ?u.15101
inst✝⁴ : Zero M
l : List M
inst✝³ : DecidablePred fun x => getD l x 0 ≠ 0
n✝ : ℕ
R : Type u_1
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
exact add_comm n 1