α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
⊢ (∑' (x : α), Set.indicator s (↑(pure a)) x) = if a ∈ s then 1 else 0
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
⊢ ↑(toOuterMeasure (pure a)) s = if a ∈ s then 1 else 0
refine' (toOuterMeasure_apply (pure a) s).trans _
case inl
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : a ∈ s
⊢ (∑' (x : α), Set.indicator s (↑(pure a)) x) = 1

case inr
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : ¬a ∈ s
⊢ (∑' (x : α), Set.indicator s (↑(pure a)) x) = 0
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
⊢ (∑' (x : α), Set.indicator s (↑(pure a)) x) = if a ∈ s then 1 else 0
split_ifs with ha
case inl
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = if b = a then 1 else 0
case inl
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : a ∈ s
⊢ (∑' (x : α), Set.indicator s (↑(pure a)) x) = 1
refine' (tsum_congr fun b => _).trans (tsum_ite_eq a 1)
no goals
case inl
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = if b = a then 1 else 0
exact ite_eq_left_iff.2 fun hb => symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)
case inr
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : ¬a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = 0
case inr
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : ¬a ∈ s
⊢ (∑' (x : α), Set.indicator s (↑(pure a)) x) = 0
refine' (tsum_congr fun b => _).trans tsum_zero
no goals
case inr
α : Type u_1
β : Type ?u.4210
γ : Type ?u.4213
a a' : α
s : Set α
ha : ¬a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = 0
exact ite_eq_right_iff.2 fun hb => ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim