complex analysis - The idea behind the proof of Riemann mapping theorem

The proof of Riemann mapping theorem (if $U\subsetneq\mathbb C$ is simply connected then it's conformally equivalent to the unit disk $D$) goes roughly as follows:

• Consider the family $F$ of all injective functions $U\rightarrow D$ taking a given point $a$ to $0$.


• Show that $F$ is nonempty.


• The map $f\mapsto |f'(a)|$ is continuous and $F$ is uniformly bounded, so by Montel's theorem there is an $f_0\in F$ maximizing $|f_0'(a)|$.


• Show that $f_0$ is onto $D$.

The two tricky bits of the proof are the second and fourth bullets. Here are the ideas behind the proofs of the two:

• We may WLOG assume $0\not\in U$. Then there is a branch $g$ of a square root defined on $U$. Then $g$ is injective, $-g(U)$ is open and disjoint from $g(U)$ so $g(U)$ is disjoint from some closed disk. The complement of that disk can be then mapped into $D$, and composing with suitable Mobius transformation maps $a$ to $0$.


• Suppose $b\in D\setminus f_0(U)$. Then the map
  $$\psi(z)=\sqrt{\frac{f_0(z)-b}{1-\overline{b}f_0(z)}}$$
  (the inside function doesn't vanish, so we can find a branch of its square root on $U$) takes $U$ into the unit disk and hence
  $$h(z)=\frac{\psi(z)-\psi(a)}{1-\overline{\psi(a)}\psi(z)}$$
  is in $F$. We then find
  
  $$|h'(a)|=\frac{1+|b|}{2\sqrt{|b|}}|f_0'(a)|>|f_0'(a)|$$
  contradicting the choice of $f_0$.

I can see the reason behind proving the former the way we do - we want to map $U$ into a set the complement of which has nonempty interior. The square root suits this perfectly since $g(U)$ and $-g(U)$ are always disjoint for a branch of square root (we could similarly take a branch of logarithm, then $g(U)$ and $g(U)+2\pi i$ are disjoint).

However, the last part of the proof feels to me like a magic trick. I thought about it several times, but I couldn't figure out anything to explain this course of action in the proof. Clearly we would like to increase a derivative somehow, but confirming this with the function constructed above requires a computational effort, not something visible at a glance.

I was wondering, how to "justify" construction of this function in the last part of the proof (possibly by some geometric argument)? Alternatively, is it possible to argue towards existence of a function with a larger derivative, without necessarily constructing it?

Answer

Think of the hyperbolic distance. A holomorphic $g \colon D \to D$ never increases the hyperbolic distance, and if there is one pair of points $a \neq b$ such that the hyperbolic distance between $g(a)$ and $g(b)$ equals the hyperbolic distance between $a$ and $b$, then $g$ is an automorphism of the disk.

So $z \mapsto z^2$ strictly decreases the hyperbolic distance. Hence, if we have a domain $V \subset D$ on which a branch $r$ of the square root is defined (in particular a simply connected domain not containing $0$), then $r$ strictly increases the hyperbolic distance between any two points in $V$. This remains true when we compose $r$ with automorphisms of $D$, since those leave hyperbolic distance invariant. Now $W = f_0(U)$ is a simply connected proper subdomain of $D$, so we can use an automorphism $T$ of $D$ to move it so that the image doesn't contain $0$, apply $r$, and then apply another automorphism $S$ of $D$, so that $(S\circ r \circ T)(0) = 0$. Then $h = S\circ r \circ T\colon W \to D$ strictly increases hyperbolic distance, and fixes $0$. That implies $\lvert h'(0)\rvert > 1$.