α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Computation α
h : b ∈ bind s (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Computation α
h : b ∈ map f s
⊢ ∃ a, a ∈ s ∧ f a = b
rw [← bind_pure] at h
no goals
α : Type u
β : Type v
γ : Type w
f : α → β
b : β
s : Computation α
h : b ∈ bind s (pure ∘ f)
⊢ ∃ a, a ∈ s ∧ f a = b
exact
  let ⟨a, as, fb⟩ := exists_of_mem_bind h
  ⟨a, as, mem_unique (ret_mem _) fb⟩