English
The toFinsupp of a cons is the sum of the singleton at 0 and the embedded toFinsupp of the rest.
Русский
ToFinsupp (x :: xs) равно единичному на 0 x plus встраиваемому toFinsupp xs.
LaTeX
$$$$ \\operatorname{toFinsupp}(x :: xs) = \\mathsf{single}\\,0\\,x + (\\operatorname{toFinsupp} xs).\\operatorname{embDomain}\\langle \\text{Nat.succ}, \\text{Nat.succ_injective} \\rangle. $$$$
Lean4
theorem toFinsupp_append {R : Type*} [AddZeroClass R] (l₁ l₂ : List R) [DecidablePred (getD (l₁ ++ l₂) · 0 ≠ 0)]
[DecidablePred (getD l₁ · 0 ≠ 0)] [DecidablePred (getD l₂ · 0 ≠ 0)] :
toFinsupp (l₁ ++ l₂) = toFinsupp l₁ + (toFinsupp l₂).embDomain (addLeftEmbedding l₁.length) :=
by
ext n
simp only [toFinsupp_apply, Finsupp.add_apply]
cases lt_or_ge n l₁.length with
| inl h =>
rw [getD_append _ _ _ _ h, Finsupp.embDomain_notin_range, add_zero]
rintro ⟨k, rfl : length l₁ + k = n⟩
cutsat
| inr h =>
rcases Nat.exists_eq_add_of_le h with ⟨k, rfl⟩
rw [getD_append_right _ _ _ _ h, Nat.add_sub_cancel_left, getD_eq_default _ _ h, zero_add]
exact Eq.symm (Finsupp.embDomain_apply _ _ _)
