mathlib

694b3f85 - chore(measure_theory): golf a proof (#11002)