Right inverse of injective

Stream: Is there code for X?

[Pedro Minicz]

Is there something equivalent to right_inverse_of_injective in mathlib?

import tactic.basic

variables {α β : Type} [nonempty α] {f : α → β}

lemma right_inverse_of_injective (hf : function.injective f) :
  ∃ g, function.right_inverse f g :=
begin
  classical,
  let g := λ b,
      if h : ∃ a, f a = b
        then classical.some h
        else classical.choice (by apply_instance),
  use g,
  intro a,
  have ha : ∃ a', f a' = f a, from ⟨a, rfl⟩,
  simp only [g, dif_pos ha],
  apply hf,
  exact classical.some_spec ha
end

[Reid Barton]

left_inverse_inv_fun

[Reid Barton]

or even injective.has_left_inverse