case refine'_1
α : Type u_1
β : Type ?u.23008
γ : Type ?u.23011
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∀ (b : α), ¬b ∈ s → Set.indicator (↑s) (↑p) b = 0

case refine'_2
α : Type u_1
β : Type ?u.23008
γ : Type ?u.23011
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∑ b in s, Set.indicator (↑s) (↑p) b = ∑ x in s, ↑p x
α : Type u_1
β : Type ?u.23008
γ : Type ?u.23011
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ↑(toOuterMeasure p) ↑s = ∑ x in s, ↑p x
refine' (toOuterMeasure_apply p s).trans ((tsum_eq_sum (s := s) _).trans _)
no goals
case refine'_1
α : Type u_1
β : Type ?u.23008
γ : Type ?u.23011
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∀ (b : α), ¬b ∈ s → Set.indicator (↑s) (↑p) b = 0
exact fun x hx => Set.indicator_of_not_mem (Finset.mem_coe.not.2 hx) _
no goals
case refine'_2
α : Type u_1
β : Type ?u.23008
γ : Type ?u.23011
p : Pmf α
s✝ t : Set α
s : Finset α
⊢ ∑ b in s, Set.indicator (↑s) (↑p) b = ∑ x in s, ↑p x
exact Finset.sum_congr rfl fun x hx => Set.indicator_of_mem (Finset.mem_coe.2 hx) _