intro ⟨_, rfl, h⟩
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
⊢ y ∈ (Set.pure a).bind f → y ∈ f a
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.6556
a : α
f : α → Set β
y : β
h : y ∈ f a
⊢ y ∈ f a