no goals
α : 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
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