-- Module: Mathlib.Probability.Martingale.OptionalStopping
Goal:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
_ :
  HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
_₁ :
  ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) +
      ENNReal.ofReal
        (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)},
          stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) =
    ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ)
_₂ :
  ENNReal.ofReal
      (∫ (ω : Ω), stoppedValue f (fun (ω : Ω) ↦ (↑(hittingBtwn f {y : ℝ | (↑ε : ℝ) ≤ y} 0 n ω) : WithTop ℕ)) ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)
⊢ HSMul.hSMul (β := ℝ≥0∞) ε
        ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑ε : ℝ) ≤ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω} : ℝ≥0∞) +
      ENNReal.ofReal (∫ (ω : Ω) in {ω : Ω | ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k ω) < (↑ε : ℝ)}, f n ω ∂μ) ≤
    ENNReal.ofReal (∫ (x : Ω), f n x ∂μ)

Tactic:
calc
    _ ≤ ENNReal.ofReal
          (∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω},
            stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) +
        ENNReal.ofReal
          (∫ ω in {ω | ((range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) < ε},
            stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by
      gcongr with ω hω
      · exact smul_le_stoppedValue_hittingBtwn hsub n
      · exact (hsub.integrable n).integrableOn
      · refine Integrable.integrableOn ?_
        refine hsub.integrable_stoppedValue ?_ (fun ω ↦ mod_cast hittingBtwn_le ω)
        exact hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici
      · exact nullMeasurableSet_lt (measurable_range_sup'' fun n _ ↦
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)).aemeasurable aemeasurable_const
      rw [Set.mem_setOf_eq] at hω
      have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by
        simp only [hittingBtwn, Set.mem_setOf_eq, ite_eq_right_iff, forall_exists_index, and_imp]
        intro m hm hεm
        exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))
      simp only [stoppedValue, this, ge_iff_le]
      refine le_of_eq ?_
      congr
    _ = ENNReal.ofReal
        (∫ ω, stoppedValue f (fun ω ↦ (hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω : ℕ)) ω ∂μ) := by
      rw [← ENNReal.ofReal_add, ← setIntegral_union]
      · rw [← setIntegral_univ (μ := μ)]
        convert! rfl
        ext ω
        change _ ↔ (ε : ℝ) ≤ _ ∨ _ < (ε : ℝ)
        simp only [le_or_gt, Set.mem_univ]
      · grind
      · exact measurableSet_lt (measurable_range_sup'' fun n _ =>
          (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)) measurable_const
      · exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))
      · exact Integrable.integrableOn (hsub.integrable_stoppedValue
          (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
          (fun ω ↦ mod_cast hittingBtwn_le ω))
      exacts [integral_nonneg fun x => hnonneg _ _, integral_nonneg fun x => hnonneg _ _]
    _ ≤ ENNReal.ofReal (μ[f n]) := by
      refine ENNReal.ofReal_le_ofReal ?_
      rw [← stoppedValue_const f n]
      refine hsub.expected_stoppedValue_mono
        (hsub.stronglyAdapted.adapted.isStoppingTime_hittingBtwn measurableSet_Ici)
        (isStoppingTime_const _ _) (fun ω ↦ ?_) (fun _ => mod_cast le_rfl)
      simp [hittingBtwn_le]

Premises used: MeasureTheory.stoppedValue, ENNReal.ofReal, Finset.nonempty_range_add_one, setOf, MeasureTheory.Measure.restrict, MeasureTheory.hittingBtwn, LE.le, Nat.cast, Finset.range, HAdd.hAdd, MeasureTheory.integral, LT.lt, Finset.sup', OfNat.ofNat, NNReal.toReal