Integral sum weight increments mem Icc

lemma integral_sum_weight_increments_mem_Icc [OrderBot ι]    (hXint : ∀ s, Integrable (X s) μ) {C : ℝ}    (hC : ∀ S : ElementaryPredictableSet 𝓕, μ[(S.indicator (1 : ℝ) ● X) t] ≤ C)    {n : ℕ} {idx : ℕ → ι} (hidx : Monotone idx) (hidxt : ∀ k, idx k ≤ t)    {W : ℕ → Ω → ℝ} (hW01 : ∀ k, k < n → ∀ ω, W k ω = 0 ∨ W k ω = 1)    (hWmeas : ∀ k, k < n → Measurable[𝓕 (idx k)] (W k)) :    ∫ ω, (∑ k ∈ range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω)) ∂μ        ∈ Set.Icc (-(C + ∫ ω, |X (idx n) ω - X (idx 0) ω| ∂μ)) C := by  have hb01 : ∀ (V : ℕ → Ω → ℝ), (∀ k, k < n → ∀ ω, V k ω = 0 ∨ V k ω = 1) →      ∀ k, k < n → ∀ ω, ‖V k ω‖ ≤ 1 := by    intro V hV k hk ω    rcases hV k hk ω with h | h <;> simp [h]  have hupper : ∀ (V : ℕ → Ω → ℝ), (∀ k, k < n → ∀ ω, V k ω = 0 ∨ V k ω = 1) →      (∀ k, k < n → Measurable[𝓕 (idx k)] (V k)) →      ∫ ω, (∑ k ∈ range n, V k ω * (X (idx (k + 1)) ω - X (idx k) ω)) ∂μ ≤ C := by    intro V hV01 hVmeas    let S := elemPredSetOfSeq hidx n hVmeas    have hS := integral_elemPredSetOfSeq (𝓕 := 𝓕) (X := X) n hidx hidxt (W := V) hV01 hVmeas    rw [← funext_iff] at hS    rw [← hS]    exact hC S  constructor  · -- lower bound via the complementary weights    have hW1 : ∀ k, k < n → ∀ ω, (1 - W k ω) = 0 ∨ (1 - W k ω) = 1 := by grind    have hW1meas : ∀ k, k < n → Measurable[𝓕 (idx k)] (fun ω ↦ 1 - W k ω) :=      fun k hk ↦ (measurable_const.sub (hWmeas k hk))    have hco := hupper (fun k ω ↦ 1 - W k ω) hW1 hW1meas    have hsplit : ∀ ω, (∑ k ∈ range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω))        = (X (idx n) ω - X (idx 0) ω)          - ∑ k ∈ range n, (1 - W k ω) * (X (idx (k + 1)) ω - X (idx k) ω) := by      intro ω      have htel : ∑ k ∈ range n, (X (idx (k + 1)) ω - X (idx k) ω)          = X (idx n) ω - X (idx 0) ω := sum_range_sub (fun k ↦ X (idx k) ω) n      rw [← htel, ← sum_sub_distrib]      grind    have hint1 : Integrable        (fun ω ↦ ∑ k ∈ range n, (1 - W k ω) * (X (idx (k + 1)) ω - X (idx k) ω)) μ :=      integrable_sum_weight_increments hXint        (fun k hk ↦ ((hW1meas k hk).mono (𝓕.le _) le_rfl).aestronglyMeasurable)        (hb01 _ hW1)    have hintsub : Integrable (fun ω ↦ X (idx n) ω - X (idx 0) ω) μ :=      (hXint _).sub (hXint _)    have hI : ∫ ω, (∑ k ∈ range n, W k ω * (X (idx (k + 1)) ω - X (idx k) ω)) ∂μ        = (∫ ω, (X (idx n) ω - X (idx 0) ω) ∂μ)          - ∫ ω, (∑ k ∈ range n, (1 - W k ω) * (X (idx (k + 1)) ω - X (idx k) ω)) ∂μ := by      rw [integral_congr_ae (μ := μ) (ae_of_all _ hsplit), integral_sub hintsub hint1]    have hT : -(∫ ω, |X (idx n) ω - X (idx 0) ω| ∂μ)        ≤ ∫ ω, (X (idx n) ω - X (idx 0) ω) ∂μ := by      rw [neg_le]      calc -∫ ω, (X (idx n) ω - X (idx 0) ω) ∂μ          ≤ |∫ ω, (X (idx n) ω - X (idx 0) ω) ∂μ| := neg_le_abs _        _ ≤ ∫ ω, |X (idx n) ω - X (idx 0) ω| ∂μ := abs_integral_le_integral_abs    rw [hI]    linarith [hco]  · exact hupper W hW01 hWmeas