bijective implies has_left_inverse

Stream: new members

[Jason KY.]

Hi, I'm trying to find a lemma in mathlib that says if a function is bijective then it has a left inverse but library_search can't seem to find it

import tactic

variables {X Y : Type}

open function

/-
example (f : X → Y) (h : bijective f) : has_left_inverse f
:= by library_search -- failed
-/

example (f : X → Y) (h : bijective f) : has_left_inverse f :=
  let ⟨hinj, hsur⟩ := h in
begin
  choose g hg using hsur,
  exact ⟨g, λ x, hinj (hg _)⟩
end

Surely this is in mathlib right?

[Bhavik Mehta]

You can use injective.has_left_inverse

[Bhavik Mehta]

And it should be easy to get bijective from injective by deconstructing the bijective if it's not already a lemma somehwere

[Reid Barton]

I don't think has_left_inverse is really used

[Jason KY.]

I've found of_bijective which does exactly what I want and helps me skip a couple of tedious steps!