mathlib

7249afb2 - feat(measure_theory/[integrable_on, set_integral]): integrals on two ae-eq sets are equal (#8440)