case h
α✝ : Type ?u.61956
α : Type u_1
a✝ : List α
⊢ (bind (range (↑card (Quotient.mk (isSetoid α) a✝) + 1)) fun k => powersetLen k (Quotient.mk (isSetoid α) a✝)) =
    powerset (Quotient.mk (isSetoid α) a✝)
α✝ : Type ?u.61956
α : Type u_1
S : Multiset α
⊢ (bind (range (↑card S + 1)) fun k => powersetLen k S) = powerset S
induction S using Quotient.inductionOn
case h
α✝ : Type ?u.61956
α : Type u_1
a✝ : List α
⊢ ↑(List.map ofList (List.bind (List.range (length a✝ + 1)) fun a => sublistsLen a a✝)) =
    ↑(List.map ofList (sublists' a✝))
case h
α✝ : Type ?u.61956
α : Type u_1
a✝ : List α
⊢ (bind (range (↑card (Quotient.mk (isSetoid α) a✝) + 1)) fun k => powersetLen k (Quotient.mk (isSetoid α) a✝)) =
    powerset (Quotient.mk (isSetoid α) a✝)
simp_rw [quot_mk_to_coe, powerset_coe', powersetLen_coe, ← coe_range, coe_bind, ← List.bind_map,
  coe_card]
no goals
case h
α✝ : Type ?u.61956
α : Type u_1
a✝ : List α
⊢ ↑(List.map ofList (List.bind (List.range (length a✝ + 1)) fun a => sublistsLen a a✝)) =
    ↑(List.map ofList (sublists' a✝))
exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)