α : Type u_1
β : Type ?u.184861
γ : Type ?u.184864
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (∑' (x : α), Set.indicator t (↑(ofMultiset s hs)) x) =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
α : Type u_1
β : Type ?u.184861
γ : Type ?u.184864
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ ↑(toOuterMeasure (ofMultiset s hs)) t =
    (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑(↑Multiset.card s)
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
α : Type u_1
β : Type ?u.184861
γ : Type ?u.184864
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
α : Type u_1
β : Type ?u.184861
γ : Type ?u.184864
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (∑' (x : α), Set.indicator t (↑(ofMultiset s hs)) x) =
    ∑' (i : α), ↑(Multiset.count i (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
refine' tsum_congr fun x => _
no goals
α : Type u_1
β : Type ?u.184861
γ : Type ?u.184864
s : Multiset α
hs : s ≠ 0
t : Set α
x : α
⊢ Set.indicator t (↑(ofMultiset s hs)) x =
    ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s)) * (↑(↑Multiset.card s))⁻¹
by_cases hx : x ∈ t <;> simp [Set.indicator, hx, div_eq_mul_inv]