no goals
α : Type u_3
β : Type u_2
γ : Type u_1
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : γ
⊢ ↑(bind (bind p f) g) b = ↑(bind p fun a => bind (f a) g) 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