finsupps of given "cardinality"

Stream: general

[Johan Commelin]

What is the idiomatic way to complete

import data.finsupp

variables (σ : Type*) [fintype σ]

def fintype_sum_id_eq (n : ℕ) :
  fintype {d : σ →₀ ℕ // d.sum (λ _, id) = n} :=
set.finite.fintype $
begin
  sorry
end

[Kenny Lau]

I mean each component can't exceed n

[Kenny Lau]

import data.finsupp

open_locale classical

variables (σ : Type*) [fintype σ]

def aux (n : ℕ) (d : {d : σ →₀ ℕ // d.sum (λ _, id) = n}) (s : σ) : fin (n+1) :=
⟨d.1 s, nat.lt_succ_of_le $ sorry⟩ -- motive incorrect

theorem aux_injective (n : ℕ) : function.injective (aux σ n) :=
λ d₁ d₂ H, subtype.eq $ finsupp.ext $ λ s, by have := congr_fun H s; convert fin.veq_of_eq this -- elaboration issues

noncomputable def fintype_sum_id_eq (n : ℕ) :
  fintype {d : σ →₀ ℕ // d.sum (λ _, id) = n} :=
fintype.of_injective (aux σ n) (aux_injective σ n)

[Kenny Lau]

Lean doesn't like me

[Johan Commelin]

Lean also doesn't like me.

[Johan Commelin]

I think we are missing some "machinery/API" here. This fact is "obvious". But not to lean.

[Johan Commelin]

There is finsupp.lt_wf, but I don't think it is of any use here.

[Johan Commelin]

With #3029 it should be easy.