cases eq_or_gt_of_le hm with
| inl hm => exists m
| inr hm_lt =>
  cases eq_or_lt_of_le hM with
  | inl hM_eq => exists M
  | inr hM_lt =>
    simp_rw [eq_comm]
    rw [← Set.mem_image]
    refine @Set.mem_of_mem_of_subset _ _ (Set.Ioo (f m) (f M)) _ ?_ ?_
    . exact And.intro hm_lt hM_lt
    . refine @IsPreconnected.intermediate_value_Ioo _ _ _ _ _ _ _
        hs_conn (nhdsWithin m s) (nhdsWithin M s) ?_ ?_ ?_ ?_ _
        hf_cont _ _ ?_ ?_
      . rw [← mem_closure_iff_nhdsWithin_neBot]
        rw [IsClosed.closure_eq hs_closed]
        exact hm_mem
      . rw [← mem_closure_iff_nhdsWithin_neBot]
        rw [IsClosed.closure_eq hs_closed]
        exact hM_mem
      . simp; exact self_mem_nhdsWithin
      . simp; exact self_mem_nhdsWithin
      . exact hf_cont m hm_mem
      . exact hf_cont M hM_mem
case inr.refine_2.intro.intro.intro.intro.intro
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
hz_ne_zero : ↑z ≠ 0
m M : ℝ
hm_mem : m ∈ s
hM_mem : M ∈ s
hm : f m ≤ (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z
hM : (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z ≤ f M
⊢ ∃ c ∈ s, (∫ (x : ℝ) in s, f x * g x ∂μ) / ↑z = f c
no goals