have hz_ne_zero : (z : ℝ) ≠ 0 := ne_of_gt hz_pos
case inr.refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z
case inr.refine_2
f g : ℝ → ℝ
s : Set ℝ
μ : Measure ℝ
hs_ne : Set.Nonempty s
hs_meas : MeasurableSet s
hs_conn : IsPreconnected s
hs_closed : IsClosed s
hf_cont : ContinuousOn f s
hg_int : IntegrableOn g s
hg_nonneg : 0 ≤ᵐ[Measure.restrict μ s] g
h_int : IntegrableOn (fun x => f x * g x) s
z : NNReal
hz' : ∫ (x : ℝ) in s, g x ∂μ = ↑z
hz : ENNReal.toNNReal (∫⁻ (x : ℝ) in s, ↑‖g x‖₊ ∂μ) = z
hz_pos : 0 < z
hmM : ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ∈ Set.Icc (f m) (f M)
hz_ne_zero : ↑z ≠ 0
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ↑z