case h.e'_2
ι : Type ?u.910499
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
x : Multiset α
⊢ (Finset.sup (Finset.range (↑card x + 1)) fun k => powersetLen k x) =
    bind (range (↑card x + 1)) fun k => powersetLen k x
ι : Type ?u.910499
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
x : Multiset α
⊢ (Finset.sup (Finset.range (↑card x + 1)) fun k => powersetLen k x) = powerset x
convert bind_powerset_len x using 1
case h.e'_2
ι : Type ?u.910499
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
x : Multiset α
⊢ (Finset.sup (Finset.range (↑card x + 1)) fun k => powersetLen k x) =
    ∑ x_1 in Finset.range (↑card x + 1), powersetLen x_1 x
case h.e'_2
ι : Type ?u.910499
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
x : Multiset α
⊢ (Finset.sup (Finset.range (↑card x + 1)) fun k => powersetLen k x) =
    bind (range (↑card x + 1)) fun k => powersetLen k x
rw [Multiset.bind, Multiset.join, ← Finset.range_val, ← Finset.sum_eq_multiset_sum]
no goals
case h.e'_2
ι : Type ?u.910499
β : Type u
α✝ : Type v
γ : Type w
s s₁ s₂ : Finset α✝
a : α✝
f g : α✝ → β
inst✝¹ : DecidableEq α✝
α : Type u_1
inst✝ : DecidableEq α
x : Multiset α
⊢ (Finset.sup (Finset.range (↑card x + 1)) fun k => powersetLen k x) =
    ∑ x_1 in Finset.range (↑card x + 1), powersetLen x_1 x
exact
  Eq.symm (finset_sum_eq_sup_iff_disjoint.mpr fun _ _ _ _ h => pairwise_disjoint_powersetLen x h)