using surjective

Stream: new members

[Pedro Castilho]

Hi, am trying to use the definition of surjection on a proof but can't quiet get what I want

example (h : surjective f) : u ⊆ f '' (f⁻¹' u) :=
begin
unfold preimage,
unfold image,
intro x,
dsimp,
intro h,
have h₁ : ∃ (a : α), f a = x, from surjective f

the error his in the last line.
i also tried using:

have h₁ : ∃ (a : α), f a = x, from exists.intro a h

could someone point my mistake?

[Yury G. Kudryashov]

..., from h x

[Yury G. Kudryashov]

surjective f is a type; h is an assumption of this type. You need to apply it to a point to get what you want.

[Yury G. Kudryashov]

BTW, after intro h you have two hypotheses with the same name.

[Yury G. Kudryashov]

You should rename one of them.

[Yury G. Kudryashov]

Also try unfold surjective at h to see the actual type behind surjective.

[Pedro Castilho]

@Yury G. Kudryashov thx for the anwser it really helped and sorry for late the late replay