How to use Type application Rule to get a desired type
You can look at this rule in two ways:

As a checking rule, it says that, to verify that $t_1 t_2$ has type $T_{12}$, we check that there exists some $T_{11}$ such that $t_1 : T_{11} \to T_{12}$, and we check that $t_2 : T_{11}$. If these checks hold, then the typing of the application must hold.

As an inference rule, it says that to infer the type of $t_1 t_2$,
we infer the type of $t_1$ and verify that it has the form $T_{11} \to T_{12}$ for some types $T_{11}, T_{12}$, infer the type for $t_2$ and check that it is equal to $T_{11}$. If these checks hold, then we return $T_{12}$ as the type of the application.

So for knowing what $T_{11}$ is, it depends on what you're doing. If you're doing checking, then usually it is a type that has already been given to you. If you're doing inference, then you infer the type of the function, and inspect that type to verify that it's an arrow type, and can be broken into its parts. $T_{11}$ is one of these parts you break it into.

There's nothing saying you need to get $T_{11}$ only from the function's type. You could alternately infer it from the type of the argument, and then verify that it matched the function type.