## 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...

#### 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