Exponential is covering map

Stream: Is there code for X?

[Lean tester]

Tried looking through these pages:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Complex/Circle.html
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Covering.html

But didn't find anything that seemed related to this particularly.

I'm looking for this after previously trying to find "lifting correspondence by the exponential map from π₁(S¹, p₀)→Z is an isomorphism" and not finding that either.

[Thomas Browning]

This PR gets close: #7596