intro y
case a
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
⊢ ∀ (x : β), x ∈ (Set.pure f).seq s ↔ x ∈ Set.map f s
case a
α : Sort u_1
β : Sort u_2
γ : ?m.9244
f : α → β
s : Set α
y : β
⊢ y ∈ (Set.pure f).seq s ↔ y ∈ Set.map f s