apply Set.ext
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
⊢ (Set.pure a).bind f = f a
case a
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
⊢ ∀ (x : β), x ∈ (Set.pure a).bind f ↔ x ∈ f a