Here are different things I have formalized in Coq.
Here is a formalization of the winding number theory and proofs of various complex analysis theorems using it.
The formalization consists of:
A definition of metric spaces and their main properties
A definition of euclidean spaces
Basics of complex analysis: continuity and differentiation, exponential and logarithm, curve integral
A definition of the winding number of a continuous lace thanks to the path lifting property.
In the cas of C1 functions, an alternative definition making use of the curve integral
The proof of homotopy invariance of the winding numbers
Classical proof (crucially relying on the notion of winding number) of the following theorems have also been formalized:
The Fundamental theorem of algebra: every complex polynomial admits at least one root
The 2-dimensional no retraction theorem
The 2-dimensional Brouwer fixed point theorem
The 2-dimensional Borsuk-Ulam theorem.