lebesgue): tidy a proof (#12274)

Commit

3 years ago

chore(measure_theory/decomposition/lebesgue): tidy a proof (#12274) There's no need to go through `set_integral_re_add_im` when all we need is `integral_re`.

Author

eric-wieser

Parents

6653544f

mathlib3 c127fc36 - chore(measure_theory/decomposition/lebesgue): tidy a proof (#12274)

mathlib3
c127fc36 - chore(measure_theory/decomposition/lebesgue): tidy a proof (#12274)