cases eq_or_gt_of_le (zero_le z) with
| inl hz_zero =>
  simp [hz_zero] at hz'
  simp [hz']
  refine And.intro hs_ne ?_
  apply integral_eq_zero_of_ae
  rw [integral_eq_zero_iff_of_nonneg_ae hg_nonneg hg_int] at hz'
  apply Filter.Eventually.mp hz'
  simp
  apply Filter.eventually_of_forall
  intro x hx
  exact Or.inr hx
| inr hz_pos =>
  have hmM := existsBoundsOn_integral_mul_nonneg hs_meas hg_int hg_nonneg ?_ h_int
  swap
  . intro h_zero
    simp [h_zero] at hz'
    rw [eq_comm] at hz'
    rw [NNReal.coe_eq_zero] at hz'
    simp [hz'] at hz_pos
  rw [hz']
  rw [hz'] at hmM
  have hz_ne_zero : (z : ℝ) ≠ 0 := ne_of_gt hz_pos
  conv => arg 1; intro c; rhs; rw [← div_eq_iff hz_ne_zero]
  rcases hmM with ⟨m, hmM⟩
  rcases hmM with ⟨M, hmM⟩
  rcases hmM with ⟨⟨hm_mem, hM_mem⟩, ⟨hm, hM⟩⟩
  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
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
⊢ ∃ c ∈ s, ∫ (x : ℝ) in s, f x * g x ∂μ = f c * ∫ (x : ℝ) in s, g x ∂μ
no goals