cases eq_or_gt_of_le (zero_le z) with
| inl hz_zero =>
  exfalso
  rw [hz_zero] at hz
  rw [ENNReal.toNNReal_eq_zero_iff] at hz
  cases hz with
  | inl _ => contradiction
  | inr h => exact ne_of_lt hq_fin h
| inr hz_pos =>
  generalize hp : (z : ENNReal)⁻¹ • q = p
  have hp_one : IsProbabilityMeasure (p.restrict s)
  . constructor
    rw [← hp]
    simp
    rw [hz']
    rw [← ENNReal.div_eq_inv_mul]
    rw [ENNReal.div_eq_one_iff]
    . simp; exact hz_pos.ne'
    . simp
  have hp_eq : ∫ x in s, f x ∂p = (∫ x in s, f x ∂q) / (z : ℝ)
  . rw [← hp]
    simp
    simp [ENNReal.toReal_inv]
    rw [inv_mul_eq_div]
  have hp_int : Integrable f (p.restrict s)
  . rw [← hp]
    simp  apply Integrable.smul_measure h_int
    simp
    apply hz_pos.ne'
  have hp_meas_compl : p.restrict s sᶜ = 0
  . rw [Measure.restrict_apply (MeasurableSet.compl hs_meas)]
    simp
  have h_lb := @exists_not_mem_null_le_integral _ _ _ _ _ hp_one hp_int hp_meas_compl
  have h_ub := @exists_not_mem_null_integral_le _ _ _ _ _ hp_one hp_int hp_meas_compl
  simp at h_lb
  simp at h_ub
  rcases h_lb with ⟨m, ⟨hm_mem, hm⟩⟩
  rcases h_ub with ⟨M, ⟨hM_mem, hM⟩⟩
  exists m
  exists M
  apply And.intro ⟨hm_mem, hM_mem⟩
  simp
  apply And.intro
  . rw [hp_eq] at hm
    exact hm
  . rw [hp_eq] at hM
    exact hM
case mk
f : ℝ → ℝ
q : Measure ℝ
s : Set ℝ
hs_meas : MeasurableSet s
hq_nonzero : ↑↑q s ≠ 0
h_int : IntegrableOn f s
z : NNReal
hz : ENNReal.toNNReal (↑↑q s) = z
hq_fin : ↑↑q s < ⊤
hz' : ↑↑q s = ↑z
⊢ ∃ m M, (m ∈ s ∧ M ∈ s) ∧ (∫ (x : ℝ) in s, f x ∂q) / ↑z ∈ Set.Icc (f m) (f M)
no goals