Proof HasLeftInverse = Injective

Stream: general

[ZHAO Jinxiang]

I want to proof

A function f with nonempty domain is injective if and only if it has a left inverse.

https://en.wikipedia.org/wiki/Inverse_function#Left_inverses

import Mathlib.Tactic
import Mathlib.Init.Function
universe u₁ u₂

variable {α : Sort u₁} {β : Sort u₂}

example (h_nonempty: Set.Nonempty (univ : Set α)) (f : α → β) : Function.HasLeftInverse f = Function.Injective f := by
  ext;
  constructor;
  · exact Function.HasLeftInverse.injective;
  · intros h1;
    use (λ y => if y ∈ (Set.range f) then sorry else sorry);
    sorry

It throws a error:

typeclass instance problem is stuck, it is often due to metavariables
  Decidable (?m.110 ∈ Set.range ?m.35769)Lean 4

What can I do to fix it?

[Yaël Dillies]

Add classical to the proof

[Eric Wieser]

You don't need any of the ;s there either

[ZHAO Jinxiang]

I also don't know how to proof it.

[Eric Wieser]

If you want to cheat... docs#Function.HasLeftInverse.injective Oh, that's the half you already found!

[Eric Wieser]

docs#Function.invFun is probably what you want to use

[Eric Wieser]

docs#Function.Injective.hasLeftInverse

[Eric Wieser]

docs#Function.injective_iff_hasLeftInverse is almost exactly your statement