Theorem ILTIS gives us a straightforward condition equivalence for an invertible linear transformation, but of course, it is even easier in Sage.
As easy as that is, it is still instructive to walk through an example similar to Example CIVLT using Sage, as a further illustration of the second half of the proof of Theorem ILTIS. Since T is surjective, every element of the codomain has a nonempty pre-image, and since T is injective, the pre-image of each element is a single element. Keep these facts in mind and convince yourself that the procedure below would never raise an error, and always has a unique result.
We first compute the pre-image of each element of a basis of the codomain.
Then we define a new linear transformation, from V to U, which turns it around and uses the preimages as a set of images defining the new linear transformation. Explain to yourself how we know that preimages is a basis for U, and why this will create an invertible linear transformation.
While this is a simple two-step procedure (form preimages, construct linear transformation), realize that this is not the process that Sage uses internally.
Notice that the essence of this construction is that when we work with an invertible linear transformation, the method .preimage_representative() behaves as a function (we mean the precise mathematical definition here) — it is always defined and always produces just one well-defined output. Here the linear_transformation() constructor is extending it to a linear function based on its action on a (finite) basis of the domain.