Extending a finsupp from a type σ to Option σ

Stream: Is there code for X?

[Antoine Chambert-Loir]

For e : σ →₀ ℕ and m : ℕ, there is a unique f : Option σ →₀ ℕthat extends e and maps none to m, for example one can set f := embDomain Function.Embedding.some e + Finsupp.single none m. Is there a simpler way to get it?
In particular, that method uses that ℕ has an addition, and this is obviously irrelevant.

[Antoine Chambert-Loir]

(This is something I fell upon in #20495.)

[Eric Wieser]

You can use update instead of addition

[Eric Wieser]

But defining this from scratch to be Option.elim is likely better

[Antoine Chambert-Loir]

Does it make sense to add the construction and a few lemmas around docs#Finsupp.some ?

[Antoine Chambert-Loir]

In any case, I adjusted #20495, see
https://github.com/leanprover-community/mathlib4/blob/3f3d91282978cae413d2503f13799a56a5afc626/Mathlib/Data/Finsupp/Basic.lean#L756-L766