no goals
α : Type u_2
β : Type u_1
γ : Type ?u.107281
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ ∃ a h, b ∈ support (f a h)
simp only [support_bindOnSupport, Set.mem_setOf_eq, Set.mem_iUnion]