α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList (sublists' l)
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ powersetLen n (Quotient.mk (isSetoid α) l) ≤ powerset (Quotient.mk (isSetoid α) l)
simp only [quot_mk_to_coe, powersetLen_coe, powerset_coe', coe_le]
no goals
α : Type u_1
n : ℕ
s : Multiset α
l : List α
⊢ List.map ofList (sublistsLen n l) <+~ List.map ofList (sublists' l)
exact ((sublistsLen_sublist_sublists' _ _).map _).subperm