no goals
α : Type u_2
β : Type u_1
γ : Type ?u.156387
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
simp only [toMeasure_apply_eq_toOuterMeasure_apply _ _ hs, toOuterMeasure_bindOnSupport_apply]