Splitting a finite list as sublists

Stream: Is there code for X?

[Antoine Chambert-Loir]

Is there a code for taking a set with at least n elements, a partition of n and obtaining a list of lists with the correct sizes and no duplicate, such as

lemma list.exists_pw_disjoint_with_card {c : list ℕ} (hc : c.sum ≤ fintype.card α) :
  ∃ (o : list (list α)),
  (list.map (list.length) o = c) ∧ (∀ s ∈ o, list.nodup s) ∧ list.pairwise list.disjoint o :=
sorry

(In fact, I proved that, but maybe I shouldn't have…)
This allowed me to characterize all cycle types of permutations on a set of given cardinality:

lemma equiv.perm_with_cycle_type_nonempty_iff {m : multiset ℕ} :
  (m.sum ≤ fintype.card α ∧ (∀ a ∈ m, 2 ≤ a)) ↔ (equiv.perm_with_cycle_type α m).nonempty :=
sorry

[Martin Dvořák]

Is (∀ s ∈ o, list.nodup s) ∧ list.pairwise list.disjoint o the same as list.nodup o.join or I got it wrong?

[Patrick Johnson]

docs#list.nodup_join

[Antoine Chambert-Loir]

That allows to simplify the statement, thanks for the link!