lift through an injective function

Stream: mathlib4

[Jireh Loreaux]

Do we have the following definition?

import Mathlib

open Set Function

variable {α β γ : Type*}
variable (f : α → γ) (g : β → γ) (hg : Injective g) (hfg : ∀ x, f x ∈ range g)

noncomputable def liftThrough (x : α) : β :=
  (Equiv.ofInjective g hg).symm ((range g).codRestrict f hfg x)

variable {f g hg hfg}

@[simp]
lemma comp_liftThrough_apply {x : α} : g (liftThrough f g hg hfg x) = f x := by
  simp [liftThrough, Equiv.apply_ofInjective_symm]

[Eric Wieser]

I think the injectivity is a distraction?

noncomputable def liftThrough (x : α) : β :=
  (hfg x).choose


@[simp]
lemma comp_liftThrough_apply {x : α} : g (liftThrough f g hfg x) = f x :=
  (hfg x).choose_spec

[Etienne Marion]

Is it the same as docs#Function.extend ?

[Jireh Loreaux]

No, it's just docs#Exists.choose