Applying a left inverse to an equation

Stream: Is there code for X?

[suhr]

I've defined the following little function:

def congr_inv {f: α → β}{g: β → α}(inv: ∀x, g (f x) = x): ∀{x y}, f x = y → x = g y :=
  λ{x _} e ↦ inv x ▸ congrArg g e

I'm pretty sure Mathlib has something similar, but I can't find it. I would like to know the name.

[Aaron Liu]

docs#Function.LeftInverse and docs#Function.RightInverse are the names by which you can find the type of your inv hypothesis