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