[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a'✝ a' : α
⊢ a' ∈ support (pure a) ↔ a' ∈ {a}
[PROOFSTEP]
simp [mem_support_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
⊢ a' ∈ support (pure a) ↔ a' = a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
⊢ ↑(toOuterMeasure (pure a)) s = if a ∈ s then 1 else 0
[PROOFSTEP]
refine' (toOuterMeasure_apply (pure a) s).trans _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
⊢ ∑' (x : α), Set.indicator s (↑(pure a)) x = if a ∈ s then 1 else 0
[PROOFSTEP]
split_ifs with ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : a ∈ s
⊢ ∑' (x : α), Set.indicator s (↑(pure a)) x = 1
[PROOFSTEP]
refine' (tsum_congr fun b => _).trans (tsum_ite_eq a 1)
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = if b = a then 1 else 0
[PROOFSTEP]
exact ite_eq_left_iff.2 fun hb => symm (ite_eq_right_iff.2 fun h => (hb <| h.symm ▸ ha).elim)
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : ¬a ∈ s
⊢ ∑' (x : α), Set.indicator s (↑(pure a)) x = 0
[PROOFSTEP]
refine' (tsum_congr fun b => _).trans tsum_zero
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
ha : ¬a ∈ s
b : α
⊢ Set.indicator s (↑(pure a)) b = 0
[PROOFSTEP]
exact ite_eq_right_iff.2 fun hb => ite_eq_right_iff.2 fun h => (ha <| h ▸ hb).elim
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ ↑↑(toMeasure (pure a)) s = ↑↑(Measure.dirac a) s
[PROOFSTEP]
rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s✝ : Set α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (if a ∈ s then 1 else 0) = Set.indicator s 1 a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
h : MeasurableSingletonClass α
⊢ Measure.toPmf (Measure.dirac a) = pure a
[PROOFSTEP]
rw [toPmf_eq_iff_toMeasure_eq, toMeasure_pure]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
⊢ ∑' (b : α) (a : β), ↑p b * ↑(f b) a = 1
[PROOFSTEP]
simp only [ENNReal.tsum_mul_left, tsum_coe, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : β
⊢ b ∈ support (bind p f) ↔ b ∈ ⋃ (a : α) (_ : a ∈ support p), support (f a)
[PROOFSTEP]
simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : β
⊢ b ∈ support (bind p f) ↔ ∃ a, a ∈ support p ∧ b ∈ support (f a)
[PROOFSTEP]
simp only [support_bind, Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
⊢ bind (pure a) f = f a
[PROOFSTEP]
have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by split_ifs with h <;> simp; subst h;
  simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
⊢ (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : a' = a
⊢ ↑(f a') b = ↑(f a) b
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : ¬a' = a
⊢ 0 = 0
[PROOFSTEP]
simp
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
b : β
a' : α
h : a' = a
⊢ ↑(f a') b = ↑(f a) b
[PROOFSTEP]
subst h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
f : α → Pmf β
b : β
a' : α
⊢ ↑(f a') b = ↑(f a') b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
⊢ bind (pure a) f = f a
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
a : α
f : α → Pmf β
this : ∀ (b : β) (a' : α), (if a' = a then ↑(f a') b else 0) = if a' = a then ↑(f a) b else 0
b : β
⊢ ↑(bind (pure a) f) b = ↑(f a) b
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
x y : α
hy : y ≠ x
⊢ ↑p y * ↑(pure y) x = 0
[PROOFSTEP]
rw [pure_apply_of_ne _ _ hy.symm, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
x : α
⊢ ↑p x * ↑(pure x) x = ↑p x
[PROOFSTEP]
rw [pure_apply_self, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f : α → Pmf β
g : β → Pmf γ
p : Pmf α
q : Pmf β
x : β
⊢ ↑(bind p fun x => q) x = ↑q x
[PROOFSTEP]
rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : γ
⊢ ↑(bind (bind p f) g) b = ↑(bind p fun a => bind (f a) g) b
[PROOFSTEP]
simpa only [ENNReal.coe_eq_coe.symm, bind_apply, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm, mul_assoc,
  mul_left_comm, mul_comm] using ENNReal.tsum_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : α → Pmf β
g : β → Pmf γ
p : Pmf α
q : Pmf β
f : α → β → Pmf γ
b : γ
⊢ ↑(bind p fun a => bind q (f a)) b = ↑(bind q fun b => bind p fun a => f a b) b
[PROOFSTEP]
simpa only [ENNReal.coe_eq_coe.symm, bind_apply, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm, mul_assoc,
  mul_left_comm, mul_comm] using ENNReal.tsum_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
⊢ ↑(toOuterMeasure (bind p f)) s = ∑' (b : β), if b ∈ s then ∑' (a : α), ↑p a * ↑(f a) b else 0
[PROOFSTEP]
simp [toOuterMeasure_apply, Set.indicator_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), ↑p a * ↑(f a) b else 0) = ∑' (a : α), ↑p a * if b ∈ s then ↑(f a) b else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
h✝ : b ∈ s
⊢ ∑' (a : α), ↑p a * ↑(f a) b = ∑' (a : α), ↑p a * ↑(f a) b
[PROOFSTEP]
simp
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
b : β
h✝ : ¬b ∈ s
⊢ 0 = ∑' (a : α), ↑p a * 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
⊢ (if b ∈ s then ↑(f a) b else 0) = if b ∈ s then ↑(f a) b else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
h✝ : b ∈ s
⊢ ↑(f a) b = ↑(f a) b
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
b : β
h✝ : ¬b ∈ s
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
s : Set β
a : α
⊢ (↑p a * ∑' (b : β), if b ∈ s then ↑(f a) b else 0) = ↑p a * ↑(toOuterMeasure (f a)) s
[PROOFSTEP]
simp only [toOuterMeasure_apply, Set.indicator_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
⊢ (∑' (b : β) (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 1
[PROOFSTEP]
refine' ENNReal.tsum_comm.trans (_root_.trans (tsum_congr fun a => _) p.tsum_coe)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
⊢ (∑' (a_1 : β), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = ↑p a
[PROOFSTEP]
simp_rw [ENNReal.tsum_mul_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
⊢ (↑p a * ∑' (i : β), if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) i) = ↑p a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
h : ↑p a = 0
⊢ ↑p a * ∑' (i : β), 0 = ↑p a
[PROOFSTEP]
simp only [h, zero_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
a : α
h : ¬↑p a = 0
⊢ ↑p a * ∑' (i : β), ↑(f a (_ : ¬↑p a = 0)) i = ↑p a
[PROOFSTEP]
rw [(f a h).tsum_coe, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
⊢ support (bindOnSupport p f) = ⋃ (a : α) (h : a ∈ support p), support (f a h)
[PROOFSTEP]
refine' Set.ext fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ b ∈ ⋃ (a : α) (h : a ∈ support p), support (f a h)
[PROOFSTEP]
simp only [ENNReal.tsum_eq_zero, not_or, mem_support_iff, bindOnSupport_apply, Ne.def, not_forall, mul_eq_zero,
  Set.mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0) ↔
    ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
[PROOFSTEP]
exact
  ⟨fun hb =>
    let ⟨a, ⟨ha, ha'⟩⟩ := hb
    ⟨a, ha, by simpa [ha] using ha'⟩,
    fun hb =>
    let ⟨a, ha, ha'⟩ := hb
    ⟨a, ⟨ha, by simpa [(mem_support_iff _ a).1 ha] using ha'⟩⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
hb : ∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0
a : α
ha : ¬↑p a = 0
ha' : ¬(if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) b) = 0
⊢ ¬↑(f a (_ : a ∈ support p)) b = 0
[PROOFSTEP]
simpa [ha] using ha'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
hb : ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
a : α
ha : ¬↑p a = 0
ha' : ¬↑(f a (_ : a ∈ support p)) b = 0
⊢ ¬(if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) b) = 0
[PROOFSTEP]
simpa [(mem_support_iff _ a).1 ha] using ha'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ ∃ a h, b ∈ support (f a h)
[PROOFSTEP]
simp only [support_bindOnSupport, Set.mem_setOf_eq, Set.mem_iUnion]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
⊢ (bindOnSupport p fun a x => f a) = bind p f
[PROOFSTEP]
ext b
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
[PROOFSTEP]
have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b := fun a =>
  ite_eq_right_iff.2 fun h => h.symm ▸ symm (zero_mul <| f a b)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
this : ∀ (a : α), (if ↑p a = 0 then 0 else ↑p a * ↑(f a) b) = ↑p a * ↑(f a) b
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
[PROOFSTEP]
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite, mul_zero, this]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ ↑(bindOnSupport p f) b = 0 ↔ ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
[PROOFSTEP]
simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∀ (i : α), ¬↑p i = 0 → (if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0)) b) = 0) ↔
    ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
[PROOFSTEP]
exact ⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha), fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
⊢ bindOnSupport (pure a) f = f a (_ : a ∈ support (pure a))
[PROOFSTEP]
refine' Pmf.ext fun b => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ ↑(bindOnSupport (pure a) f) b = ↑(f a (_ : a ∈ support (pure a))) b
[PROOFSTEP]
simp only [bindOnSupport_apply, pure_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ (∑' (a_1 : α),
      (if a_1 = a then 1 else 0) *
        if h : (if a_1 = a then 1 else 0) = 0 then 0 else ↑(f a_1 (_ : ¬↑(pure a) a_1 = 0)) b) =
    ↑(f a (_ : a ∈ support (pure a))) b
[PROOFSTEP]
refine' _root_.trans (tsum_congr fun a' => _) (tsum_ite_eq a _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
[PROOFSTEP]
by_cases h : a' = a
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
h : a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
h : ¬a' = a
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
⊢ (bindOnSupport p fun a x => pure a) = p
[PROOFSTEP]
simp only [Pmf.bind_pure, Pmf.bindOnSupport_eq_bind]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
⊢ bindOnSupport (bindOnSupport p f) g =
    bindOnSupport p fun a ha => bindOnSupport (f a ha) fun b hb => g b (_ : b ∈ support (bindOnSupport p f))
[PROOFSTEP]
refine' Pmf.ext fun a => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ ↑(bindOnSupport (bindOnSupport p f) g) a =
    ↑(bindOnSupport p fun a ha => bindOnSupport (f a ha) fun b hb => g b (_ : b ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
dsimp only [bindOnSupport_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ (∑' (a_1 : β),
      (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) *
        if h : (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = 0 then 0 else ↑(g a_1 h) a) =
    ∑' (a_1 : α),
      ↑p a_1 *
        if h : ↑p a_1 = 0 then 0
        else
          ∑' (a_2 : β),
            ↑(f a_1 h) a_2 * if h : ↑(f a_1 h) a_2 = 0 then 0 else ↑(g a_2 (_ : a_2 ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
simp only [← tsum_dite_right, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) a_1) *
        if h : (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = 0 then 0 else ↑(g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      ↑p a_1 *
        if h : ↑p a_1 = 0 then 0
        else ↑(f a_1 h) i * if h : ↑(f a_1 h) i = 0 then 0 else ↑(g i (_ : i ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
simp only [ENNReal.tsum_eq_zero, dite_eq_left_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) a_1) *
        if h : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) a_1) = 0 then 0
        else ↑(g a_1 (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) a_1) = 0)) a) =
    ∑' (a_1 : α) (i : β),
      ↑p a_1 *
        if h : ↑p a_1 = 0 then 0
        else ↑(f a_1 h) i * if h : ↑(f a_1 h) i = 0 then 0 else ↑(g i (_ : i ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
refine' ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
⊢ ((↑p a' * if h : ↑p a' = 0 then 0 else ↑(f a' h) b) *
      if h : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0 then 0
      else ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a) =
    ↑p a' *
      if h : ↑p a' = 0 then 0
      else ↑(f a' h) b * if h : ↑(f a' h) b = 0 then 0 else ↑(g b (_ : b ∈ support (bindOnSupport p f))) a
[PROOFSTEP]
split_ifs with h _ h_1 _ h_2
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * 0 = ↑p a' * 0
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a = ↑p a' * 0
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * 0)
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * 0)
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
any_goals ring1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * 0 = ↑p a' * 0
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ↑p a' = 0
_ : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
⊢ ↑p a' * 0 * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a = ↑p a' * 0
[PROOFSTEP]
ring1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * 0)
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
ring1
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * 0)
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
ring1
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
have := h_1 a'
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
this : (↑p a' * if h : ↑p a' = 0 then 0 else ↑(f a' h) b) = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
simp [h] at this 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
_ : ¬↑(f a' h) b = 0
this : ↑(f a' (_ : ¬↑p a' = 0)) b = 0
⊢ ↑p a' * ↑(f a' h) b * 0 = ↑p a' * (↑(f a' h) b * ↑(g b (_ : b ∈ support (bindOnSupport p f))) a)
[PROOFSTEP]
contradiction
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
g : (b : β) → b ∈ support (bindOnSupport p f) → Pmf γ
a : γ
a' : α
b : β
h : ¬↑p a' = 0
h_1 : ¬∀ (i : α), (↑p i * if h : ↑p i = 0 then 0 else ↑(f i h) b) = 0
h_2 : ↑(f a' h) b = 0
⊢ ↑p a' * ↑(f a' h) b * ↑(g b (_ : ¬(∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) = 0)) a =
    ↑p a' * (↑(f a' h) b * 0)
[PROOFSTEP]
simp [h_2]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ (bindOnSupport p fun a ha => bindOnSupport q (f a ha)) =
    bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb
[PROOFSTEP]
apply Pmf.ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ ∀ (x : γ),
    ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) x =
      ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) x
[PROOFSTEP]
rintro c
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) c =
    ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) c
[PROOFSTEP]
simp only [ENNReal.coe_eq_coe.symm, bindOnSupport_apply, ← tsum_dite_right, ENNReal.tsum_mul_left.symm,
  ENNReal.tsum_mul_right.symm]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ (∑' (a : α) (i : β),
      ↑p a *
        if h : ↑p a = 0 then 0 else ↑q i * if h : ↑q i = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) i (_ : ¬↑q i = 0)) c) =
    ∑' (a : β) (i : α),
      ↑q a * if h : ↑q a = 0 then 0 else ↑p i * if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0) a (_ : ¬↑q a = 0)) c
[PROOFSTEP]
refine' _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => _)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
⊢ (↑p a * if h : ↑p a = 0 then 0 else ↑q b * if h : ↑q b = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c) =
    ↑q b * if h : ↑q b = 0 then 0 else ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c
[PROOFSTEP]
split_ifs with h1 h2 h2
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ↑p a = 0
h2 : ↑q b = 0
⊢ ↑p a * 0 = ↑q b * 0
[PROOFSTEP]
ring
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ↑p a = 0
h2 : ¬↑q b = 0
⊢ ↑p a * 0 = ↑q b * (↑p a * 0)
[PROOFSTEP]
ring
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ¬↑p a = 0
h2 : ↑q b = 0
⊢ ↑p a * (↑q b * 0) = ↑q b * 0
[PROOFSTEP]
ring
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
h1 : ¬↑p a = 0
h2 : ¬↑q b = 0
⊢ ↑p a * (↑q b * ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c) =
    ↑q b * (↑p a * ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c)
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ ↑(toOuterMeasure (bindOnSupport p f)) s = ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(toOuterMeasure (f a h)) s
[PROOFSTEP]
simp only [toOuterMeasure_apply, Set.indicator_apply, bindOnSupport_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
⊢ (∑' (x : β), if x ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) x else 0) =
    ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ∑' (x : β), if x ∈ s then ↑(f a (_ : ¬↑p a = 0)) x else 0
[PROOFSTEP]
calc
  (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
      ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    tsum_congr fun b => by split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]
  _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 := ENNReal.tsum_comm
  _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
  _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
    tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ∑' (a : α), if b ∈ s then ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0
[PROOFSTEP]
split_ifs with hbs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
hbs : b ∈ s
⊢ (∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b) =
    ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b
[PROOFSTEP]
simp only [eq_self_iff_true, tsum_zero]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
b : β
hbs : ¬b ∈ s
⊢ 0 = ∑' (a : α), 0
[PROOFSTEP]
simp only [eq_self_iff_true, tsum_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
⊢ (∑' (b : β), if b ∈ s then ↑p a * if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ↑p a * ∑' (b : β), if b ∈ s then if h : ↑p a = 0 then 0 else ↑(f a h) b else 0
[PROOFSTEP]
simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
⊢ (↑p a * ∑' (b : β), if b ∈ s then if h : ↑p a = 0 then 0 else ↑(f a h) b else 0) =
    ↑p a * if h : ↑p a = 0 then 0 else ∑' (b : β), if b ∈ s then ↑(f a h) b else 0
[PROOFSTEP]
split_ifs with ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
ha : ↑p a = 0
⊢ (↑p a * ∑' (b : β), if b ∈ s then 0 else 0) = ↑p a * 0
[PROOFSTEP]
simp only [ite_self, tsum_zero, eq_self_iff_true]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
a : α
ha : ¬↑p a = 0
⊢ (↑p a * ∑' (b : β), if b ∈ s then ↑(f a ha) b else 0) = ↑p a * ∑' (b : β), if b ∈ s then ↑(f a ha) b else 0
[PROOFSTEP]
simp only [ite_self, tsum_zero, eq_self_iff_true]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
s : Set β
inst✝ : MeasurableSpace β
hs : MeasurableSet s
⊢ ↑↑(toMeasure (bindOnSupport p f)) s = ∑' (a : α), ↑p a * if h : ↑p a = 0 then 0 else ↑↑(toMeasure (f a h)) s
[PROOFSTEP]
simp only [toMeasure_apply_eq_toOuterMeasure_apply _ _ hs, toOuterMeasure_bindOnSupport_apply]
