## Stream: general

### Topic: finsupps of given "cardinality"

#### Johan Commelin (Jun 09 2020 at 15:38):

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 (Jun 09 2020 at 15:44): I mean each component can't exceed n #### Kenny Lau (Jun 09 2020 at 16:01): 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 (Jun 09 2020 at 16:01):

Lean doesn't like me

#### Johan Commelin (Jun 09 2020 at 16:40):

Lean also doesn't like me.

#### Johan Commelin (Jun 09 2020 at 16:41):

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

#### Johan Commelin (Jun 09 2020 at 17:03):

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

#### Johan Commelin (Jun 11 2020 at 13:49):

With #3029 it should be easy.

Last updated: May 14 2021 at 22:15 UTC