Smallness of the DFinsupp type

Let π : ι → Type v. If ι and all the π i are w-small, this provides a Small.{w} instance on DFinsupp π.

As an application, σ →₀ R has a Small.{v} instance if σ and R have one.

instance DFinsupp.small {ι : Type u} {π : ι → Type v} [(i : ι) → Zero (π i)] [Small.{w, u} ι] [∀ (i : ι), Small.{w, v} (π i)] : Small.{w, max v u} (DFinsupp π)

instance Finsupp.small {σ : Type u_1} {R : Type u_2} [Zero R] [Small.{u, u_2} R] [Small.{u, u_1} σ] : Small.{u, max u_2 u_1} (σ →₀ R)