It seems to me that the following proposition should be a case for `iinv`

or other codomain-, image-, or `injective`

-related library lemmas, but I'm not able to find one that seems to work:

```
Lemma f_surj
n (lt0n : 0 < n)
(T : finType) (cardT : #|T| = n.+1) (t : n.-tuple T)
(f : 'I_n -> T) (injf : injective f) (fint : forall i : 'I_n, f i \in t) g :
g \in t -> exists i : 'I_n, f i = g.
```

Any suggestion .... or proof that it is wrong? ;)

Seems you can drop that T is finite, it only needs decidable equality to implement a search over I_n?

If the search failed, that'd imply having n + 1 distinct elements of t, so you'll need a pigeonhole lemma

I'm sorry I can't help further; but I hope that's a helpful proof sketch at least

The statement of surjectivity looks a bit weird to me but here is one way to prove it :

```
Lemma f_surj n (T : eqType) (t : n.-tuple T)
(f : 'I_n -> T) (injf : injective f) (fint : forall i : 'I_n, f i \in t) g :
g \in t -> exists i : 'I_n, f i = g.
Proof.
suff <- : codom f =i t by case/codomP => i ->; exists i.
have [|y /codomP[i ->]//||//] :=
uniq_min_size _ (_ : {subset (codom f) <= t}) _.
by rewrite map_inj_uniq // enum_uniq.
by rewrite size_map size_enum_ord size_tuple.
Qed.
```

Thanks a lot @Laurent Théry and @Paolo Giarrusso. The lemma is indeed a bit weird (thanks for the simplification of the hypothesis, also), since it's a somewhat generalized version of a property I need within a proof related to matching problems.

Last updated: Jul 15 2024 at 21:02 UTC