no goals
α : Type u_1
β : Type u_2
γ : Type ?u.62680
p✝ : Pmf α
f : α → Pmf β
g : β → Pmf γ
p : Pmf α
q : Pmf β
x : β
⊢ ↑(bind p fun x => q) x = ↑q x
rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]