Difficulty with dif_pos

Stream: new members

[Valentin Vinoles]

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]

You need to unfold the definition of g first with simp only [g]

[Jireh Loreaux]

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]

have h' :/have h :, you mean, I assume?

[Valentin Vinoles]

Yeah sorry, I mixed up h et h', it should be fixed now.

[Valentin Vinoles]

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]

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

[Valentin Vinoles]

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

[Valentin Vinoles]

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