lifting functions

Stream: general

[Kevin Buzzard]

If I have f : X -> Y, an injection i : Z -> Y and a proof that for all x : X, f x \in range i then as a mathematician I would say that I can lift f to a function X -> Z. Unfortunately lift is used for something else in Lean. What is this operation called in Lean? And is it in Lean already? I guess it's noncomputable.

[David Michael Roberts]

something using the word 'factor'?