Confusing type mismatch

Stream: new members

[Trevor Hyde]

I'm making a Lean file to demonstrate proving some basic properties of functions. I'm running into a type mismatch error when I try to unpack the hf_surj : ∀ y, ∃ x, f x = y assumption using cases'. Below I have my code followed by my error message. Help?

variable {X Y : Type} {f : X → Y}
def is_surjective (f : X → Y) : Prop :=
  ∀ y, ∃ x, f x = y

-- other preliminary stuff

theorem inverse_iff_bijective (f : X → Y) : has_inverse f ↔ is_bijective f := by
  constructor
  · sorry
  · rintro ⟨hf_inj,hf_surj⟩
    use (fun y => by
      specialize hf_surj y
      cases' hf_surj with x hx
      done)
    done
  done

type mismatch when assigning motive
  fun t => hf_surj = t → X
has type
  (∃ x, f x = y) → Type : Type 1
but is expected to have type
  (∃ x, f x = y) → Prop : Type

[Aaron Liu]

You can't deconstruct an existential hypothesis when constructing data. The solution is to use docs#Classical.choose or docs#Exists.choose.

[Aaron Liu]

Your code is not a #mwe. It would be better to post a #mwe as that increases the chance that someone will help you.