mathlib3

c7d6e642 - chore(measure_theory/measure/giry_monad): add spaces, golf (#17155)

chore(measure_theory/measure/giry_monad): add spaces, golf (#17155) Minor changes: add spaces after lambdas, squeeze some simps (one of which was non-terminal), golf a proof...