constructor
case a
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) ↔ y ∈ Set.pure (f a)
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.map f (Set.pure a) → y ∈ Set.pure (f a)

case a.mpr
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
⊢ y ∈ Set.pure (f a) → y ∈ Set.map f (Set.pure a)