no goals
α : Type u_2
β : Type u_1
γ : Type ?u.56378
p : Pmf α
f : α → Pmf β
g : β → Pmf γ
b : β
⊢ b ∈ support (bind p f) ↔ ∃ a, a ∈ support p ∧ b ∈ support (f a)
simp only [support_bind, Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]