Formal Notation for Finding Inverses of Functions Generally in most introductory university courses, finding the inverses of functions, is done in what seems to be to be a very haphazard way.
Given any scalar function $f : \mathbb{R^n} \to \mathbb{R}$, what most people would do is say (and I put this here in as general a form as I can) :
$$y = f(x)$$
and then do a swap of variables
$$x = f^{-1}(y)$$
But the only reason this 'swap' is done is because the function $f$ is mapping a set $A$ (it's domain) to another set $B$ (it's codomain). This can be represented as $$f : A \to B$$
and the inverse is simply $$f^{-1} : B \to A$$
But the swap of the of the variables only implicitly shows this, transformation of the function $f$ to $f^{-1}$, it does not formally show the reversal of the mapping of the sets (the domain and codomain).
I will give an example below to further illustrate my point :

Example : Find $f^{-1}(x)\ \  \text{of} \ \  f(x)=e^x$
This is what most professors, typically would do to find the inverse :
$$y = f(x)$$
$$\implies y = e^x$$
$$\implies x = e^y$$
$$\implies ln(x) = ln(e^y)$$
$$\implies y = ln(x)$$
$$\implies f^{-1}(x) = ln(x)$$

As you can see in the example above, there is virtually no structure to the way the inverse function $f^{-1}$ has been computed, and leaves a lot to be desired in terms of formalism. This way of computing inverse functions, is what is commonly used by almost everyone, but I don't find it rigorous. Sure it does find the inverse function, but the process of finding it is very informal and unsatisfactory.
My question is, what is the most formal notation/process for finding the inverses of functions? Given the example above (or a more general example), how would you go about finding the inverse $f^{-1}$ in the most formal and mathematically rigorous way? Furthermore how would you go about finding the inverse of functions in higher mathematics, (e.g in Category Theory)?
 A: What you're complaining about is just an algorithm for finding the inverse. There are other such algorithms, for instance the row-reduction process for computing the inverse of a linear transformation in linear algebra. It's generally a bit misguided to expect an algorithm to be formal and rigorous: the point of an algorithm is to get the right answer. More frequently, you just want to know how to prove that whatever answer you've "guessed" with the algorithm is correct. A little bit closer to what you seem to want would be to formalize your algorithm and prove that it's correct. A formalization of the algorithm you describe would involve starting with $x=f(f^{-1}(x))$ and repeatedly composing both sides with various other functions, for instance logarithms as in your example. It's straightforward to prove that an equation holds if and only if it holds after composition with an invertible function, so the correctness of the process follows. As mentioned in the comments, you should really complicate this with consideration of domains.
But, as I suggested at first, all that's really important is that you can rigorously check that the algorithm puts out the right answer, i.e. that $e^{\ln x}=x=\ln e^x$. This is usually just a definition in this case, but in general will involve various algebraic manipulations whose correctness depends in the last analysis on the associativity, commutativity, and distributivity of addition and multiplication of real numbers. 
There's no general process for computing inverses in category theory, since a category doesn't assume any particular structure to its "functions," usually called morphisms. In fact, there's no general process even for computing inverses of functions of a real variable, contrary to what you've seen with examples like the one you gave. Indeed, what's the inverse of $x^5+x+1$? You have no way to "compute" it explicitly, but it's quite easy to show that it must be invertible. Since the latter is so much more generally possible, that's where we tend to focus our requests for rigor.
