theorem Function.Injective.leftInverse {α : Sort u_1} {β : Sort u_2} (f : α → β) (hf : Injective f) [hα : Nonempty α] : ∃ (g : β → α), LeftInverse g f

noncomputable def Lean.Grind.leftInv {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Injective f) [Nonempty α] : β → α

theorem Lean.Grind.leftInv_eq {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Injective f) [Nonempty α] (a : α) : f⁻¹ (f a) = a

def Lean.Grind.leftInvUnexpander : PrettyPrinter.Unexpander