  We describe the formalization of the existence and uniqueness of Haar measure
in the Lean theorem prover. The Haar measure is an invariant regular measure on
locally compact groups, and it has not been formalized in a proof assistant
before. We will also discuss the measure theory library in Lean's mathematical
library \textsf{mathlib}, and discuss the construction of product measures and
the proof of Fubini's theorem for the Bochner integral.
