cases h
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
y : β
x : α
hx : x ∈ s
h : f x = y
⊢ y ∈ f <$> t
case refl
α : Type u_1
s t u : Set α
β : Type u_1
f : α → β
hst : s.Subset t
x : α
hx : x ∈ s
⊢ f x ∈ f <$> t