Please formalize the statement and proof in Lean4 that the fundamental group of the circle is isomorphic to the integers.