integrals w.r.t. lebesgue_measure and completed_lebesgue_measure agree

[screenl]

Lemma lebesgue_borel_int_eq (f : R -> \bar R) :
  measurable_fun (T := g_sigma_algebraType (R.-ocitv.-measurable)) setT f ->
  \int[lebesgue_measure]_x f x = \int[completed_lebesgue_measure]_x f x.

Is there a way to do this proof? eq_measure_integral does not seem to work because the measure_display is not the same.