generalize hz : ENNReal.toNNReal (q s) = z
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑(ENNReal.toNNReal (↑↑q s)) ∈ Set.Icc (f m) (f M)
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_fin : IsFiniteMeasure (Measure.restrict q s)
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)