Mul integral upcrossings Before fin Idx le

lemma mul_integral_upcrossingsBefore_finIdx_le [OrderBot ι] [IsFiniteMeasure μ]    (hX : Adapted 𝓕 X) (hXint : ∀ s, Integrable (X s) μ) {C : ℝ}    (hC : ∀ S : ElementaryPredictableSet 𝓕, μ[(S.indicator 1 ● X) t] ≤ C)    (hab : a < b) (hF : ∀ s ∈ F, s ≤ t) :    (b - a) * ∫ ω, (upcrossingsBefore a b (fun k ↦ X (finIdx F t k)) #F ω : ℝ) ∂μ      ≤ C + ∫ ω, (a - X t ω)⁺ ∂μ := 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)  let S := elemPredSetOfSeq (W := upcrossingStrat a b f #F) (finIdx_monotone hF) #F fun k hk ↦    (hadapt.upcrossingStrat k).measurable  have hintS : Integrable ((S.indicator (1 : ℝ) ● X) t) μ :=    ElementaryPredictableSet.integrable_integral_real hXint S 1 t  have hintmax : Integrable (fun ω ↦ (a - X t ω)⁺) μ :=    (((integrable_const a).sub (hXint t))).pos_part  have hintcount : Integrable (fun ω ↦ (upcrossingsBefore a b f #F ω : ℝ)) μ :=    hadapt.integrable_upcrossingsBefore hab  calc (b - a) * ∫ ω, (upcrossingsBefore a b f #F ω : ℝ) ∂μ  _ = ∫ ω, (b - a) * (upcrossingsBefore a b f #F ω : ℝ) ∂μ := (integral_const_mul _ _).symm  _ ≤ ∫ ω, ((S.indicator (1 : ℝ) ● X) t ω + (a - X t ω)⁺) ∂μ :=    integral_mono (hintcount.const_mul _) (hintS.add hintmax)      (mul_upcrossingsBefore_le_integral_add_posPart hX.stronglyAdapted hab hF)  _ = μ[(S.indicator (1 : ℝ) ● X) t] + ∫ ω, (a - X t ω)⁺ ∂μ := integral_add hintS hintmax  _ ≤ C + ∫ ω, (a - X t ω)⁺ ∂μ := by gcongr; exact hC S