rw [←h]
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ y ∈ Set.pure (f a)
case a.mp
α : Sort u_2
β : Sort u_1
γ : ?m.5720
f : α → β
a : α
y : β
h : f a = y
⊢ f a ∈ Set.pure (f a)