constructor
case a
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) ↔ y ∈ Set.map f s
case a.mp
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ (y ∈ s.bind fun x => Set.pure (f x)) → y ∈ Set.map f s

case a.mpr
α : Sort u_1
β : Sort u_2
γ : ?m.8715
f : α → β
s : Set α
y : β
⊢ y ∈ Set.map f s → y ∈ s.bind fun x => Set.pure (f x)