α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList (sublists l)
α : Type u_1
s : Multiset α
l : List α
⊢ map singleton (Quotient.mk (isSetoid α) l) ≤ powerset (Quotient.mk (isSetoid α) l)
simp only [powerset_coe, quot_mk_to_coe, coe_le, coe_map]
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ List.ret) l <+~ List.map ofList (sublists l)
α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList (sublists l)
show l.map (((↑) : List α → Multiset α) ∘ List.ret) <+~ (sublists l).map (↑)
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map List.ret l) <+~ List.map ofList (sublists l)
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ List.ret) l <+~ List.map ofList (sublists l)
rw [← List.map_map]
no goals
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map List.ret l) <+~ List.map ofList (sublists l)
exact ((map_ret_sublist_sublists _).map _).subperm