chore(MeasureTheory/Integral/IntervalIntegral/MeanValue): update for Lean's new module system

Author: Deep0Thinking

Mathlib/MeasureTheory/Integral/IntervalIntegral/MeanValue.lean

@@ -3,7 +3,9 @@ Copyright (c) 2025 Louis (Yiyang) Liu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Louis (Yiyang) Liu
 -/
-import Mathlib.MeasureTheory.Integral.IntervalAverage
+module
+
+public import Mathlib.MeasureTheory.Integral.IntervalAverage
 
 /-!
 # First mean value theorem for integrals
@@ -35,6 +37,8 @@ and one assuming pointwise nonnegativity together with continuity of `g`.
 mean value theorem, interval integral, measure, nonnegative, continuous, integrable
 -/
 
+@[expose] public section
+
 open MeasureTheory Set intervalIntegral
 
 /-- **First mean value theorem for integrals (interval integral, arbitrary measure).**