I am looking for a reference or proof of the following property of a Riemannian manifold $M$: if $M$ is not simply connected, then it contains a non-trivial closed curve of minimum length. I am fine with making assumptions about $M$ such as compact, smooth, analytic etc.
I have elementary knowledge of differential geometry. Based on the definition of a simply connected manifold I know that a closed curve cannot be continuously deformed to a point. However, I do not know how to formalize this procedure, or why some sequence of deformations should converge or even result in a reduction of the length of the curve.
Edit: The manifold needs to be closed. I am looking for a proof that on a closed but not simply connected Riemannian manifold there exists at least one closed curve (or closed geodesic) which is a local minimum of the length function in the space of smooth curves.
Based on the newest edit, I've made some adaptations.
First, if $M$ is not compact, the result is not true. As said in the comments, the punctured plane with the induced metric is an example.
If $M$ is compact, the result is true. In fact, we have that the following is true:
Those loops are necessarily geodesics, by variational reasons.
One way to see why this is true is via a Morse-theory approach, with a full proof being given in Klingenberg - Lectures on Closed Geodesics. The gist of it is to pick a loop close to the infimum on the class and flow it under (minus) the gradient flow of the energy functional in the free loop space (this has an obvious analogy with the finite-dimensional case when we flow via gradient and converge to a critical point).
To see how the result we mentioned implies what you want, just notice that a variation of a geodesic stays in the same class. Thus, if the geodesic minimizes length on the class, it is a local minimizer.
EDIT: The book by Klingenberg gives a reference which does not use the machinery behind the proof I alluded to above. He says:
He attributes the proof (in special cases) to Hadamard and Cartan (although he says that the later has an error), and says that Berger - Lectures on geodesics in Riemannian geometry has a full proof following this idea (I have not seen it).