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

Equations

• f⁻¹ = Classical.choose ⋯

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

Equations

• One or more equations did not get rendered due to their size.