Inverses
When defining the inverse of a functions $f : \alpha \to \beta$, we run into two problems
First, it is possible that for some $y$ of type $\beta$, there exists no $x$ such that $f(x) = y$. Then, we want to assign some kind of default element to $\alpha$, such that $inverse f x = \text{default}$. We do this with the annotation
Inhabited α
Second, it is possible that there exists multiple $x$ such that $f(x) = y$. Then, we need to pick one of them. If we have a context and goal as
y : β
h : ∃ x : α, f x = y
⊢ f (inverse f y) = y
Then we can prove the goal with
exact inverse_spec y h