no goals
α : Type u_1
β : Type ?u.116357
γ : Type ?u.116360
p✝ : Pmf α
f : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
⊢ (bindOnSupport p fun a x => pure a) = p
simp only [Pmf.bind_pure, Pmf.bindOnSupport_eq_bind]