Solution (source code)

= Solution

Write $M=|f(z_0)|$. The local maximum property gives a <disk> around $z_0$ on which $|f|\leq M$, contained in the <unit disk>. If $M=0$, then $f=0$ on that neighbourhood, and the <identity theorem> makes $f$ zero on the connected <unit disk>.

Otherwise multiply $f$ by the unit <complex number> $\overline{f(z_0)}/M$, obtaining a <holomorphic function> $g$ with $g(z_0)=M$ and $|g|\leq M$ nearby. Applying the <Cauchy integral formula> on any sufficiently small circle of radius $r$ gives the <mean value property>
$$
M=\frac1{2\pi}\int_0^{2\pi}g(z_0+re^{it})\,dt.
$$
Take real parts. The continuous function $M-\operatorname{Re}g$ is nonnegative on the circle and has <integral> zero, so it vanishes everywhere there. Since $|g|\leq M$, having real part $M$ forces imaginary part zero. Thus $g=M$ throughout the circle. The zeros of $g-M$ have an accumulation point inside its domain, so the <identity theorem> gives \b[$f$ constant on the entire <unit disk>]. This proves the local <maximum modulus principle> directly from the <Cauchy integral formula>.