Measure Real alt Set le

lemma measureReal_altSet_le [OrderBot ι] [IsFiniteMeasure μ]    (hX : Adapted 𝓕 X) (hXint : ∀ s, Integrable (X s) μ) {C : ℝ}    (hC : ∀ S : ElementaryPredictableSet 𝓕, μ[(S.indicator (1 : ℝ) ● X) t] ≤ C)    (hab : a < b) (hm : 0 < m) (hF : ∀ s ∈ F, s ≤ t) :    μ.real (altSet X F a b m) ≤ (C + ∫ ω, (a - X t ω)⁺ ∂μ) / (b - a) / m := by  let f : ℕ → Ω → ℝ := fun k ω ↦ X (finIdx F t k) ω  have hadapt : StronglyAdapted (𝓕.indexComap (finIdx_monotone hF)) f :=    Adapted.stronglyAdapted <| fun j ↦ hX (finIdx F t j)  rw [altSet_eq_upcrossingsBefore (t := t) hab, div_div, le_div_iff₀ (by positivity)]  calc μ.real {ω | m ≤ upcrossingsBefore a b f #F ω} * ((b - a) * m)  _ = μ.real {ω | (m : ℝ) ≤ (upcrossingsBefore a b f #F ω : ℝ)} * ((b - a) * m) := by norm_cast  _ = (b - a) * ((m : ℝ) * μ.real {ω | (m : ℝ) ≤ (upcrossingsBefore a b f #F ω : ℝ)}) := by ring  _ ≤ (b - a) * ∫ ω, (upcrossingsBefore a b f #F ω : ℝ) ∂μ := by    gcongr    exact mul_meas_ge_le_integral_of_nonneg      (ae_of_all _ fun ω ↦ by positivity) (hadapt.integrable_upcrossingsBefore hab) m  _ ≤ C + ∫ ω, (a - X t ω)⁺ ∂μ :=    mul_integral_upcrossingsBefore_finIdx_le (μ := μ) hX hXint hC hab hF