  We report on a formalization of the change of variables formula in integrals,
in the mathlib library for Lean. Our version of this theorem is extremely
general, and builds on developments in linear algebra, analysis, measure theory
and descriptive set theory. The interplay between these domains is transparent
thanks to the highly integrated development model of mathlib.
