# Zulip Chat Archive

## Stream: new members

### Topic: Difficulty with dif_pos

#### Valentin Vinoles (Dec 01 2023 at 19:56):

Hello

I am trying to prove that if a function is injective then it has a left inverse. What I have done so far:

```
import Mathlib
noncomputable section
open Classical
open Function
variable {α β : Type}[Inhabited α]
def is_left_inverse (g : β → α)(f : α → β) : Prop :=
∀ x, g (f x) = x
def has_left_inverse (f: α → β) : Prop :=
∃ g : β → α, is_left_inverse g f
variable (f : α → β)
example (h : Injective f) : has_left_inverse f := by
let g : β → α := fun y => (if h : ∃ x, y = f x then h.choose else default)
use g
intro x -- ⊢ g (f x) = x
have h' : ∃ x', f x = f x' := by use x
rw [dif_pos h']
```

The function `g`

is the inverse (I got it from "mathematics in Lean"). So now I want to prove `g( f x) = x`

.

I understood that I should use `dif_pos`

to compute `g(f x)`

but `rw [dif_pos h]`

does not work here and I do not understand why...

Thanks for your help !

#### Jireh Loreaux (Dec 01 2023 at 20:02):

You need to unfold the definition of `g`

first with `simp only [g]`

#### Jireh Loreaux (Dec 01 2023 at 20:03):

Also, you're going to want to do `have h' :`

instead of `have h :`

because you already have a hypothesis named `h`

.

#### Yaël Dillies (Dec 01 2023 at 20:04):

`have h' :`

/`have h :`

, you mean, I assume?

#### Valentin Vinoles (Dec 01 2023 at 20:07):

Yeah sorry, I mixed up `h`

et `h'`

, it should be fixed now.

#### Valentin Vinoles (Dec 01 2023 at 20:12):

I tried `simp only [g]`

but it does not work (Lean tells me invalid 'simp', proposition expected `β → α`

and I am not sure what is going on) but it seems that using just `simp`

works ? Because if I do:

```
-- same code as before until have h' : .... (included)
simp
rw [dif_pos h']
```

the goal is now `⊢ Exists.choose h' = x`

.

Thanks, I am making some (slow) progress.

#### Jireh Loreaux (Dec 01 2023 at 20:16):

Are you on and older version of Lean? This was fixed within the last month I believe.

#### Valentin Vinoles (Dec 01 2023 at 20:51):

Ho you are right, I just updated Lean and it works now, thanks !

#### Valentin Vinoles (Dec 01 2023 at 21:54):

I post my solution, now it works (it might be not the best one, any suggestion is welcome) :

```
example (h : Injective f) : has_left_inverse f := by
let g : β → α := fun y => (if h : ∃ x, y = f x then h.choose else default)
use g
intro x -- ⊢ g (f x) = x
have h' : ∃ x', f x = f x' := by
use x
simp only [g]
rw [dif_pos h']
have h'' := Exists.choose_spec h'
apply h at h''
exact h''.symm
```

Last updated: Dec 20 2023 at 11:08 UTC